Support for 64-bit architectures: update the PowerPC port

The PowerPC port remains 32-bit only, no support is added for PPC 64.
This shows how much work is needed to update an existing port a minima.

1 files changed, 0 insertions, 456 deletions

diff --git a/driver/Ctydescr.ml b/driver/Ctydescr.ml
deleted file mode 100644
index 8091257b..00000000
--- a/driver/Ctydescr.ml
+++ /dev/null
@@ -1,456 +0,0 @@
-open Printf
-open Camlcoq
-open Tydesc
-
-let check ty x = TyIO.check x ty; true
-  
-(* From stdlib *)
-
-let list t = List t
-let pair t1 t2 = Tuple [t1;t2]
-
-let rec repr_nat = Sum("nat", [
-  "O", [];
-  "S", [repr_nat]
-])
-
-let nat = Base {
-  base_name = "nat";
-  base_check = check repr_nat;
-  base_parse = (fun synt s -> assert false);
-  base_print = (fun synt x ->
-    let s = string_of_int (Nat.to_int x) in
-    match synt with
-    | `Coq -> s ^ "%nat"
-    |  _   -> s)
-}
-
-let rec repr_positive = Sum("positive", [
-  "xI", [repr_positive];
-  "xO", [repr_positive];
-  "xH", []
-])
-
-let positive = Base {
-  base_name = "positive";
-  base_check = check repr_positive;
-  base_parse = (fun synt s -> assert false);
-  base_print = (fun synt x -> Z.to_string (Z.Zpos x))
-}
-
-let repr_N = Sum("N", [
-  "N0", [];
-  "Npos", [repr_positive]
-])
-
-let _N = Base {
-  base_name = "N";
-  base_check = check repr_N;
-  base_parse = (fun synt s -> assert false);
-  base_print = (fun synt x ->
-    let y = match x with N.N0 -> Z.Z0 | N.Npos p -> Z.Zpos p in
-    let s = Z.to_string y in
-    match synt with
-    | `Coq -> s ^ "%N"
-    |  _   -> s)
-}
-
-let repr_Z = Sum("Z", [
-  "Z0", [];
-  "Zpos", [repr_positive];
-  "Zneg", [repr_positive]
-])
-
-let _Z = Base {
-  base_name = "Z";
-  base_check = check repr_Z;
-  base_parse = (fun synt s -> assert false);
-  base_print = (fun synt x ->
-    let s = Z.to_string x in
-    match synt with
-    | `Coq -> s ^ "%Z"
-    |  _   -> s)
-}
-
-(* From Integers *)
-
-let int = Base {
-  base_name = "int";
-  base_check = check repr_Z;
-  base_parse = (fun synt s ->
-    let (n, s') = get_number s in
-    try (coqint_of_camlint (Int32.of_string n), s')
-    with Failure _ ->
-      raise (Parsing_failure(get_position s, sprintf "bad 'int' literal %S" n)));
-  base_print = (fun synt x ->
-    let s = Z.to_string x in
-    match synt with
-    | `Coq -> "(mkint " ^ s ^ "%Z)"
-    |  _   -> s)
-}
-
-let int64 = Base {
-  base_name = "int64";
-  base_check = check repr_Z;
-  base_parse = (fun synt s ->
-    let (n, s') = get_number s in
-    try (coqint_of_camlint64 (Int64.of_string n), s')
-    with Failure _ ->
-      raise (Parsing_failure(get_position s, sprintf "bad 'int64' literal %S" n)));
-  base_print = (fun synt x ->
-    let s = Z.to_string x in
-    match synt with
-    | `Coq -> "(mkint64 " ^ s ^ "%Z)"
-    |  _   -> s)
-}
-
-(* From Floats *)
-
-let nan_pl = positive
-
-let binary_float = Sum("binary_float", [
-  "B754_zero", [bool];
-  "B754_infinity", [bool];
-  "B754_nan", [bool; nan_pl];
-  "B754_finite", [bool; positive; _Z]
-])
-
-let float = Base {
-  base_name = "float";
-  base_check = check binary_float;
-  base_parse = (fun synt s ->
-    let (n, s') = get_number s in
-    try (Floats.Float.of_bits (coqint_of_camlint64 (Int64.of_string n)), s')
-    with Failure _ ->
-      raise (Parsing_failure(get_position s, sprintf "bad 'float' literal %S" n)));
-  base_print = (fun synt x ->
-    let s = Z.to_string (Floats.Float.to_bits x) in
-    match synt with
-    | `Coq -> "(mkfloat " ^ s ^ "%Z)"
-    |  _   -> s)
-}
-
-let float32 = Base {
-  base_name = "float32";
-  base_check = check binary_float;
-  base_parse = (fun synt s ->
-    let (n, s') = get_number s in
-    try (Floats.Float32.of_bits (coqint_of_camlint (Int32.of_string n)), s')
-    with Failure _ ->
-      raise (Parsing_failure(get_position s, sprintf "bad 'float32' literal %S" n)));
-  base_print = (fun synt x ->
-    let s = Z.to_string (Floats.Float.to_bits x) in
-    match synt with
-    | `Coq -> "(mkfloat32 " ^ s ^ "%Z)"
-    |  _   -> s)
-}
-
-(* From Maps *)
-
-let ptree a =
-  let rec t = Sum(sprintf "PTree.t[%s]" (describe_ty a), [
-    "Leaf", [];
-    "Node", [t; option a; t]
-  ]) in t
-
-(* From AST *)
-
-let ident = positive
-
-let typ = Sum("typ", [
-  "AST.Tint", [];
-  "AST.Tfloat", [];
-  "AST.Tlong", [];
-  "AST.Tsingle", [];
-  "AST.Tany32", [];
-  "AST.Tany64", [];
-])
-
-let calling_convention = Record("calling_convention", [
-  "cc_vararg", bool;
-  "cc_structret", bool;
-])
-
-let default_calling_convention = {
-  dfl_val = AST.cc_default;
-  dfl_print = (function `Coq -> Some "cc_default" | _ -> None)
-}
-
-let calling_convention_d =
-  Default(calling_convention, default_calling_convention)
-
-let signature = Record("signature", [
-  "sig_args", list typ;
-  "sig_res", option typ;
-  "sig_cc", calling_convention_d;
-])
-
-let memory_chunk = Sum("memory_chunk", [
-  "Mint8signed", [];
-  "Mint8unsigned", [];
-  "Mint16signed", [];
-  "Mint16unsigned", [];
-  "Mint32", [];
-  "Mint64", [];
-  "Mfloat32", [];
-  "Mfloat64", [];
-  "Many32", [];
-  "Many64", [];
-])
-
-let init_data = Sum("init_data", [
-  "Init_int8", [int];
-  "Init_int16", [int];
-  "Init_int32", [int];
-  "Init_int64", [int64];
-  "Init_float32", [float32];
-  "Init_float64", [float];
-  "Init_space", [_Z];
-  "Init_addrof", [ident; int];
-])
-
-let globvar v = Record(sprintf "globvar[%s]" (describe_ty v), [
-  "gvar_info", v;
-  "gvar_init", list init_data;
-  "gvar_readonly", bool;
-  "gvar_volatile", bool;
-])
-
-let globdef f v = Sum(sprintf "globdef[%s][%s]" (describe_ty f) (describe_ty v), [
-  "Gfun", [f];
-  "Gvar", [globvar v];
-])
-
-let external_function = Sum("external_function", [
-  "EF_external", [ident; signature];
-  "EF_builtin", [ident; signature];
-  "EF_vload", [memory_chunk];
-  "EF_vstore", [memory_chunk];
-  "EF_vload_global", [memory_chunk; ident; int];
-  "EF_vstore_global", [memory_chunk; ident; int];
-  "EF_malloc", [];
-  "EF_free", [];
-  "EF_memcpy", [_Z; _Z];
-  "EF_annot", [ident; list typ];
-  "EF_annot_val", [ident; typ];
-  "EF_inline_asm", [ident; signature; list string];
-])
-
-(* From Values *)
-
-let block = positive
-
-let val_ = Sum("val", [
-  "Vundef", [];
-  "Vint", [int];
-  "Vlong", [int64];
-  "Vfloat", [float];
-  "Vsingle", [float32];
-  "Vptr", [block; int];
-])
-
-(* From Ctypes *)
-
-let signedness = Sum("signedness", [
-  "Signed", [];
-  "Unsigned", [];
-])
-
-let intsize = Sum("intsize", [
-  "I8", [];
-  "I16", [];
-  "I32", [];
-  "IBool", [];
-])
-
-let floatsize = Sum("floatsize", [
-  "F32", [];
-  "F64", [];
-])
-
-let attr = Record("attr", [
-  "attr_volatile", bool;
-  "attr_alignas", option _N;
-])
-
-let attr_default = {
-  dfl_val = Ctypes.noattr;
-  dfl_print = (function `Coq -> Some "noattr" | _ -> None)
-}
-
-let attr_d = Default(attr, attr_default)
-
-let rec type_ = Sum("type", [
-  "Tvoid", [];
-  "Tint", [intsize; signedness; attr_d];
-  "Tlong", [signedness; attr_d];
-  "Tfloat", [floatsize; attr_d];
-  "Tpointer", [type_; attr_d];
-  "Tarray", [type_; _Z; attr_d];
-  "Tfunction", [typelist; type_; calling_convention_d];
-  "Tstruct", [ident; attr_d];
-  "Tunion", [ident; attr_d];
-])
-and typelist = Sum("typelist", [
-  "Tnil", [];
-  "Tcons", [type_; typelist];
-])
-
-let  struct_or_union = Sum("struct_or_union", [
-  "Struct", [];
-  "Union", [];
-])
-
-let members = list (pair ident type_)
-
-let composite_definition = Sum("composite_definition", [
-  "Composite", [ident; struct_or_union; members; attr_d];
-])
-
-let composite = Record("composite",[
-  "co_su", struct_or_union;
-  "co_members", members;
-  "co_attr", attr;
-  "co_sizeof", _Z;
-  "co_alignof", _Z;
-  "co_rank", nat
-])
-
-let composite_env = ptree composite
-
-(* From Cop *)
-
-let unary_operation = Sum("unary_operation", [
-  "Onotbool", [];
-  "Onotint", [];
-  "Oneg", [];
-  "Oabsfloat", [];
-])
-
-let binary_operation = Sum("binary_operation", [
-  "Oadd", [];
-  "Osub", [];
-  "Omul", [];
-  "Odiv", [];
-  "Omod", [];
-  "Oand", [];
-  "Oor", [];
-  "Oxor", [];
-  "Oshl", [];
-  "Oshr", [];
-  "Oeq", [];
-  "One", [];
-  "Olt", [];
-  "Ogt", [];
-  "Ole", [];
-  "Oge", [];
-])
-
-let incr_or_decr = Sum("incr_or_decr", [
-  "Incr", [];
-  "Decr", [];
-])
-
-(* From Csyntax *)
-
-let rec expr = Sum("expr", [
-  "Eval", [val_; type_];
-  "Evar", [ident; type_];
-  "Efield", [expr; ident; type_];
-  "Evalof", [expr; type_];
-  "Ederef", [expr; type_];
-  "Eaddrof", [expr; type_];
-  "Eunop", [unary_operation; expr; type_];
-  "Ebinop", [binary_operation; expr; expr; type_];
-  "Ecast", [expr; type_];
-  "Eseqand", [expr; expr; type_];
-  "Eseqor", [expr; expr; type_];
-  "Econdition", [expr; expr; expr; type_];
-  "Esizeof", [type_; type_];
-  "Ealignof", [type_; type_];
-  "Eassign", [expr; expr; type_];
-  "Eassignop", [binary_operation; expr; expr; type_; type_];
-  "Epostincr", [incr_or_decr; expr; type_];
-  "Ecomma", [expr; expr; type_];
-  "Ecall", [expr; exprlist; type_];
-  "Ebuiltin", [external_function; typelist; exprlist; type_];
-  "Eloc", [block; int; type_];
-  "Eparen", [expr; type_; type_];
-])
-and exprlist = Sum("exprlist", [
-  "Enil", [];
-  "Econs", [expr; exprlist];
-])
-
-let label = ident
-
-let rec statement = Sum("statement", [
-  "Sskip", [];
-  "Sdo", [expr];
-  "Ssequence", [statement; statement];
-  "Sifthenelse", [expr; statement; statement];
-  "Swhile", [expr; statement];
-  "Sdowhile", [expr; statement];
-  "Sfor", [statement; expr; statement; statement];
-  "Sbreak", [];
-  "Scontinue", [];
-  "Sreturn", [option expr];
-  "Sswitch", [expr; labeled_statements];
-  "Slabel", [label; statement];
-  "Sgoto", [label];
-])
-and labeled_statements = Sum("labeled_statements", [
-  "LSnil", [];
-  "LScons", [option _Z; statement; labeled_statements];
-])
-
-let function_ = Record("function", [
-  "fn_return", type_;
-  "fn_callconv", calling_convention_d;
-  "fn_params", list (pair ident type_);
-  "fn_vars", list (pair ident type_);
-  "fn_body", statement;
-])
-
-let fundef = Sum("fundef", [
-  "Internal", [function_];
-  "External", [external_function; typelist; type_; calling_convention_d];
-])
-
-let repr_program = Record("program", [
-  "prog_defs", list (pair ident (globdef fundef type_));
-  "prog_public", list ident;
-  "prog_main", ident;
-  "prog_types", list composite_definition;
-  "prog_comp_env", composite_env
-])
-
-type program2 = Program of
-   (AST.ident * (Csyntax.fundef, Ctypes.coq_type) AST.globdef) list
- * AST.ident list
- * AST.ident
- * Ctypes.composite_definition list
-
-let program2 = Sum("program2", [
-  "mkprogram", [list (pair ident (globdef fundef type_));
-                list ident;
-                ident;
-                list composite_definition]
-])
-
-let program2_of_program p =
-  Csyntax.(Program(p.prog_defs, p.prog_public, p.prog_main, p.prog_types))
-let program_of_program2 (Program(d,p,m,t)) =
-  Csyntax.(
-    match Ctypes.build_composite_env t with
-    | Errors.Error _ -> assert false
-    | Errors.OK e -> {prog_defs = d; prog_public = p; prog_main = m;
-                      prog_types = t; prog_comp_env = e})
-
-let program = As(program2, {
-  conv_name = "program";
-  conv_check = check repr_program;
-  conv_out = program2_of_program;
-  conv_in = program_of_program2
-})
-