summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/PrintAsm.ml6
-rw-r--r--backend/CMparser.mly21
-rw-r--r--backend/CMtypecheck.ml2
-rw-r--r--backend/Coloringaux.ml8
-rw-r--r--backend/PrintCminor.ml4
-rw-r--r--backend/PrintLTL.ml2
-rw-r--r--backend/PrintRTL.ml2
-rw-r--r--backend/RTLgenaux.ml2
-rw-r--r--backend/RTLtypingaux.ml6
-rw-r--r--cfrontend/C2C.ml25
-rw-r--r--cfrontend/PrintClight.ml16
-rw-r--r--cfrontend/PrintCsyntax.ml16
-rw-r--r--driver/Interp.ml25
-rw-r--r--extraction/extraction.v7
-rw-r--r--ia32/PrintAsm.ml10
-rw-r--r--lib/Camlcoq.ml24
-rw-r--r--powerpc/PrintAsm.ml6
17 files changed, 80 insertions, 102 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 50b585e..a616cc2 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -201,7 +201,7 @@ let call_helper oc fn dst arg1 arg2 =
let moves =
Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in
List.iter
- (fun (Coq_pair(s, d)) ->
+ (fun (s, d) ->
fprintf oc " mov %a, %a\n" ireg d ireg s)
moves;
(* Call the helper function *)
@@ -689,7 +689,7 @@ let print_function oc name fn =
fprintf oc " .type %a, %%function\n" print_symb name;
fprintf oc " .size %a, . - %a\n" print_symb name print_symb name
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
match defn with
| Internal code ->
print_function oc name code
@@ -729,7 +729,7 @@ let rec log2 n =
assert (n > 0);
if n = 1 then 0 else 1 + log2 (n lsr 1)
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
match v.gvar_init with
| [] -> ()
| _ ->
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 0b48c0f..3df3f54 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -141,7 +141,7 @@ let mkswitch expr (cases, dfl) =
let rec mktable = function
| [] -> []
| (key, exit) :: rem ->
- Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
+ (coqint_of_camlint key, exitnum exit) :: mktable rem in
prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
(***
@@ -166,7 +166,7 @@ let mkmatch_aux expr cases =
| [] -> assert false
| [key, action] -> []
| (key, action) :: rem ->
- Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+ (coqint_of_camlint key, nat_of_camlint n)
:: mktable (Int32.succ n) rem in
let sw =
Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
@@ -324,8 +324,8 @@ global_declarations:
global_declaration:
VAR STRINGLIT LBRACKET INTLIT RBRACKET
- { Coq_pair($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
- gvar_readonly = false; gvar_volatile = false}) }
+ { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+ gvar_readonly = false; gvar_volatile = false}) }
;
proc_list:
@@ -345,14 +345,13 @@ proc:
{ let tmp = !temporaries in
temporaries := [];
temp_counter := 0;
- Coq_pair($1,
- Internal { fn_sig = $6;
- fn_params = List.rev $3;
- fn_vars = List.rev (tmp @ $9);
- fn_stackspace = $8;
- fn_body = $10 }) }
+ ($1, Internal { fn_sig = $6;
+ fn_params = List.rev $3;
+ fn_vars = List.rev (tmp @ $9);
+ fn_stackspace = $8;
+ fn_body = $10 }) }
| EXTERN STRINGLIT COLON signature
- { Coq_pair($2, External(EF_external($2, $4))) }
+ { ($2, External(EF_external($2, $4))) }
;
signature:
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 819f269..e3a6f70 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -351,7 +351,7 @@ let type_function id f =
with Error s ->
raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s))
-let type_fundef (Coq_pair (id, fd)) =
+let type_fundef (id, fd) =
match fd with
| Internal f -> type_function id f
| External ef -> ()
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 34fab90..ab7d141 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -410,11 +410,11 @@ let build g typenv spillcosts =
n in
(* Fill the adjacency set and the adjacency lists; compute the degrees. *)
SetRegReg.fold
- (fun (Coq_pair(r1, r2)) () ->
+ (fun (r1, r2) () ->
addEdge (find_reg_node r1) (find_reg_node r2))
g.interf_reg_reg ();
SetRegMreg.fold
- (fun (Coq_pair(r1, mr2)) () ->
+ (fun (r1, mr2) () ->
addEdge (find_reg_node r1) (find_mreg_node mr2))
g.interf_reg_mreg ();
(* Process the moves and insert them in worklistMoves *)
@@ -427,11 +427,11 @@ let build g typenv spillcosts =
n2.movelist <- m :: n2.movelist;
DLinkMove.insert m worklistMoves in
SetRegReg.fold
- (fun (Coq_pair(r1, r2)) () ->
+ (fun (r1, r2) () ->
add_move (find_reg_node r1) (find_reg_node r2))
g.pref_reg_reg ();
SetRegMreg.fold
- (fun (Coq_pair(r1, mr2)) () ->
+ (fun (r1, mr2) () ->
let r1' = find_reg_node r1 in
if List.mem mr2 !allocatable_registers then
add_move r1' (find_mreg_node mr2))
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 6a74506..30884b1 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -223,7 +223,7 @@ let rec print_stmt p s =
| Sswitch(e, cases, dfl) ->
fprintf p "@[<v 2>switch (%a) {" print_expr e;
List.iter
- (fun (Coq_pair(n, x)) ->
+ (fun (n, x) ->
fprintf p "@ case %ld: exit %d;\n"
(camlint_of_coqint n) (camlint_of_nat x))
cases;
@@ -262,7 +262,7 @@ let print_function p id f =
print_stmt p f.fn_body;
fprintf p "@;<0 -2>}@]@ "
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
match fd with
| External ef ->
() (* Todo? *)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 3bfd803..94f5af0 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -103,7 +103,7 @@ let print_function pp f =
List.sort
(fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
(List.map
- (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+ (fun (pc, i) -> (camlint_of_positive pc, i))
(PTree.elements f.fn_code)) in
print_succ pp f.fn_entrypoint
(match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 620a949..985bd63 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -96,7 +96,7 @@ let print_function pp f =
List.sort
(fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
(List.map
- (fun (Coq_pair(pc, i)) -> (camlint_of_positive pc, i))
+ (fun (pc, i) -> (camlint_of_positive pc, i))
(PTree.elements f.fn_code)) in
print_succ pp f.fn_entrypoint
(match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l);
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 82cb300..0822587 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -29,7 +29,7 @@ module IntSet = Set.Make(IntOrd)
let normalize_table tbl =
let rec norm keys accu = function
| [] -> (accu, keys)
- | Datatypes.Coq_pair(key, act) :: rem ->
+ | (key, act) :: rem ->
if IntSet.mem key keys
then norm keys accu rem
else norm (IntSet.add key keys) ((key, act) :: accu) rem
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 17acbc6..5935605 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -39,7 +39,7 @@ let rec set_types rl tyl =
(* First pass: process constraints of the form typeof(r) = ty *)
-let type_instr retty (Coq_pair(pc, i)) =
+let type_instr retty (pc, i) =
match i with
| Inop(_) ->
()
@@ -48,7 +48,7 @@ let type_instr retty (Coq_pair(pc, i)) =
| Iop(op, args, res, _) ->
if two_address_op op && List.length args >= 1 && List.hd args <> res
then raise (Type_error "two-address constraint violation");
- let (Coq_pair(targs, tres)) = type_of_operation op in
+ let (targs, tres) = type_of_operation op in
set_types args targs; set_type res tres
| Iload(chunk, addr, args, dst, _) ->
set_types args (type_of_addressing addr);
@@ -119,7 +119,7 @@ let type_pass1 retty instrs =
let rec extract_moves = function
| [] -> []
- | Coq_pair(pc, i) :: rem ->
+ | (pc, i) :: rem ->
match i with
| Iop(Omove, [r1], r2, _) ->
(r1, r2) :: extract_moves rem
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2f50a0e..f35598c 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -132,9 +132,8 @@ let global_for_string s id =
:: !init in
add_char '\000';
for i = String.length s - 1 downto 0 do add_char s.[i] done;
- Datatypes.Coq_pair(id,
- {gvar_info = typeStringLiteral s; gvar_init = !init;
- gvar_readonly = true; gvar_volatile = false})
+ (id, {gvar_info = typeStringLiteral s; gvar_init = !init;
+ gvar_readonly = true; gvar_volatile = false})
let globals_for_strings globs =
Hashtbl.fold
@@ -151,8 +150,7 @@ let register_special_external name ef targs tres =
let declare_special_externals k =
Hashtbl.fold
- (fun name fd k ->
- Datatypes.Coq_pair(intern_string name, fd) :: k)
+ (fun name fd k -> (intern_string name, fd) :: k)
special_externals_table k
(** ** Handling of stubs for variadic functions *)
@@ -720,7 +718,7 @@ let convertFundef env fd =
(fun (id, ty) ->
if Cutil.is_composite_type env ty then
unsupported "function parameter of struct or union type";
- Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+ (intern_string id.name, convertTyp env ty))
fd.fd_params in
let vars =
List.map
@@ -729,7 +727,7 @@ let convertFundef env fd =
unsupported "'static' or 'extern' local variable";
if init <> None then
unsupported "initialized local variable";
- Datatypes.Coq_pair(intern_string id.name, convertTyp env ty))
+ (intern_string id.name, convertTyp env ty))
fd.fd_locals in
let body' = convertStmt env fd.fd_body in
let id' = intern_string fd.fd_name.name in
@@ -739,9 +737,8 @@ let convertFundef env fd =
a_type = Cutil.fundef_typ fd;
a_fundef = Some fd };
Sections.define_function env id' fd.fd_ret;
- Datatypes.Coq_pair(id',
- Internal {fn_return = ret; fn_params = params;
- fn_vars = vars; fn_body = body'})
+ (id', Internal {fn_return = ret; fn_params = params;
+ fn_vars = vars; fn_body = body'})
(** External function declaration *)
@@ -758,7 +755,7 @@ let convertFundecl env (sto, id, ty, optinit) =
if List.mem_assoc id.name builtins.functions
then EF_builtin(id', sg)
else EF_external(id', sg) in
- Datatypes.Coq_pair(id', External(ef, args, res))
+ (id', External(ef, args, res))
(** Initializers *)
@@ -810,10 +807,8 @@ let convertGlobvar env (sto, id, ty, optinit) =
let a = Cutil.attributes_of_type env ty in
let volatile = List.mem C.AVolatile a in
let readonly = List.mem C.AConst a && not volatile in
- Datatypes.Coq_pair(id',
- {gvar_info = ty'; gvar_init = init';
- gvar_readonly = readonly;
- gvar_volatile = volatile})
+ (id', {gvar_info = ty'; gvar_init = init';
+ gvar_readonly = readonly; gvar_volatile = volatile})
(** Convert a list of global declarations.
Result is a pair [(funs, vars)] where [funs] are
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index ad6887c..306224b 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -231,17 +231,17 @@ let print_function p id f =
f.fn_return);
fprintf p "@[<v 2>{@ ";
List.iter
- (fun (Coq_pair(id, ty)) ->
+ (fun (id, ty) ->
fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
f.fn_vars;
List.iter
- (fun (Coq_pair(id, ty)) ->
+ (fun (id, ty) ->
fprintf p "register %s;@ " (name_cdecl (temp_name id) ty))
f.fn_temps;
print_stmt p f.fn_body;
fprintf p "@;<0 -2>}@]@ @ "
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
match fd with
| External(_, args, res) ->
fprintf p "extern %s;@ @ "
@@ -314,17 +314,17 @@ and collect_cases = function
let collect_function f =
collect_type f.fn_return;
- List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
- List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
- List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_temps;
+ List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+ List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
+ List.iter (fun (id, ty) -> collect_type ty) f.fn_temps;
collect_stmt f.fn_body
-let collect_fundef (Coq_pair(id, fd)) =
+let collect_fundef (id, fd) =
match fd with
| External(_, args, res) -> collect_type_list args; collect_type res
| Internal f -> collect_function f
-let collect_globvar (Coq_pair(id, v)) =
+let collect_globvar (id, v) =
collect_type v.gvar_info
let collect_program p =
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 6358786..f0e9ee5 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -312,7 +312,7 @@ let name_function_parameters fun_name params =
| _ ->
let rec add_params first = function
| [] -> ()
- | Coq_pair(id, ty) :: rem ->
+ | (id, ty) :: rem ->
if not first then Buffer.add_string b ", ";
Buffer.add_string b (name_cdecl (extern_atom id) ty);
add_params false rem in
@@ -328,13 +328,13 @@ let print_function p id f =
f.fn_return);
fprintf p "@[<v 2>{@ ";
List.iter
- (fun (Coq_pair(id, ty)) ->
+ (fun (id, ty) ->
fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
f.fn_vars;
print_stmt p f.fn_body;
fprintf p "@;<0 -2>}@]@ @ "
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
match fd with
| External(_, args, res) ->
fprintf p "extern %s;@ @ "
@@ -374,7 +374,7 @@ let print_init p = function
let re_string_literal = Str.regexp "__stringlit_[0-9]+"
-let print_globvar p (Coq_pair(id, v)) =
+let print_globvar p (id, v) =
let name1 = extern_atom id in
let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in
let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in
@@ -469,16 +469,16 @@ and collect_cases = function
let collect_function f =
collect_type f.fn_return;
- List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
- List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
+ List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+ List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
collect_stmt f.fn_body
-let collect_fundef (Coq_pair(id, fd)) =
+let collect_fundef (id, fd) =
match fd with
| External(_, args, res) -> collect_type_list args; collect_type res
| Internal f -> collect_function f
-let collect_globvar (Coq_pair(id, v)) =
+let collect_globvar (id, v) =
collect_type v.gvar_info
let collect_program p =
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 43f569c..ff097c9 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -78,7 +78,7 @@ let print_event p = function
let name_of_fundef prog fd =
let rec find_name = function
| [] -> "<unknown function>"
- | Coq_pair(id, fd') :: rem ->
+ | (id, fd') :: rem ->
if fd = fd' then extern_atom id else find_name rem
in find_name prog.prog_funct
@@ -131,7 +131,7 @@ let compare_mem m1 m2 =
if m1 == m2 then 0 else
let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else
compare_Z_range Z0 m1.Mem.nextblock (fun b ->
- let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in
+ let ((lo, hi) as bnds) = m1.Mem.bounds b in
let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else
let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in
if contents1 == contents2 then 0 else
@@ -328,7 +328,7 @@ let rec world = Determinism.World(world_io, world_vload, world_vstore)
and world_io id args =
match chop_stub(extern_atom id), args with
| "printf", EVptr_global(id, ofs) :: args' ->
- Some(Coq_pair(EVint Integers.Int.zero, world))
+ Some(EVint Integers.Int.zero, world)
| _, _ ->
None
@@ -342,7 +342,7 @@ and world_vload chunk id ofs =
| Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl))
| Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0))
| Mfloat64 -> EVfloat(Random.float 1.0)
- in Some(Coq_pair(res, world))
+ in Some(res, world)
and world_vstore chunk id ofs v =
assert !random_volatiles;
@@ -390,7 +390,7 @@ let do_step p prog ge time s =
fprintf p "@].";
exit 126
| l ->
- List.iter (fun (Coq_pair(t, s')) -> do_events p ge time s t) l;
+ List.iter (fun (t, s') -> do_events p ge time s t) l;
List.map snd l
let rec explore p prog ge time ss =
@@ -405,14 +405,17 @@ let rec explore p prog ge time ss =
explore p prog ge (time + 1) ss'
end
+(* Massaging the source program *)
+
let unvolatile prog =
- let unvolatile_globvar (Coq_pair(id, gv)) =
- Coq_pair(id,
- if gv.gvar_volatile
- then {gv with gvar_readonly = false; gvar_volatile = false}
- else gv) in
+ let unvolatile_globvar (id, gv) =
+ (id, if gv.gvar_volatile
+ then {gv with gvar_readonly = false; gvar_volatile = false}
+ else gv) in
{prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
+(* Execution of a whole program *)
+
let execute prog =
Random.self_init();
let p = err_formatter in
@@ -420,5 +423,5 @@ let execute prog =
let prog' = if !random_volatiles then prog else unvolatile prog in
begin match Cexec.do_initial_state prog' with
| None -> fprintf p "ERROR: Initial state undefined@."
- | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s)
+ | Some(ge, s) -> explore p prog ge 0 (StateSet.singleton s)
end
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 4bfac69..52706ab 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -19,11 +19,8 @@ Require Compiler.
Require Initializers.
(* Standard lib *)
-Extract Inductive unit => "unit" [ "()" ].
-Extract Inductive bool => "bool" [ "true" "false" ].
-Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inductive option => "option" [ "Some" "None" ].
-Extract Inductive list => "list" [ "[]" "(::)" ].
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlString.
(* Float *)
Extract Inlined Constant Floats.float => "float".
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index f48b808..5ca56d7 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -114,7 +114,7 @@ let addressing oc (Addrmode(base, shift, cst)) =
| Coq_inl n ->
let n = camlint_of_coqint n in
fprintf oc "%ld" n
- | Coq_inr(Coq_pair(id, ofs)) ->
+ | Coq_inr(id, ofs) ->
let ofs = camlint_of_coqint ofs in
if ofs = 0l
then symbol oc id
@@ -123,8 +123,8 @@ let addressing oc (Addrmode(base, shift, cst)) =
begin match base, shift with
| None, None -> ()
| Some r1, None -> fprintf oc "(%a)" ireg r1
- | None, Some(Coq_pair(r2,sc)) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc
- | Some r1, Some(Coq_pair(r2,sc)) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc
+ | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc
+ | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc
end
let name_of_condition = function
@@ -730,7 +730,7 @@ let print_function oc name code =
jumptables := []
end
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
match defn with
| Internal code -> print_function oc name code
| External ef -> ()
@@ -761,7 +761,7 @@ let print_init_data oc name id =
else
List.iter (print_init oc) id
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
match v.gvar_init with
| [] -> ()
| _ ->
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 34aaa0f..cfbca6e 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -109,27 +109,11 @@ let extern_atom a =
(* Strings *)
-let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
- Char.chr( (if a0 then 1 else 0)
- + (if a1 then 2 else 0)
- + (if a2 then 4 else 0)
- + (if a3 then 8 else 0)
- + (if a4 then 16 else 0)
- + (if a5 then 32 else 0)
- + (if a6 then 64 else 0)
- + (if a7 then 128 else 0))
-
-let coqstring_length s =
- let rec len accu = function
- | String0.EmptyString -> accu
- | String0.String(_, s) -> len (accu + 1) s
- in len 0 s
-
-let camlstring_of_coqstring s =
- let r = String.create (coqstring_length s) in
+let camlstring_of_coqstring (s: char list) =
+ let r = String.create (List.length s) in
let rec fill pos = function
- | String0.EmptyString -> r
- | String0.String(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+ | [] -> r
+ | c :: s -> r.[pos] <- c; fill (pos + 1) s
in fill 0 s
(* Timing facility *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 3b90ada..91dd686 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -920,7 +920,7 @@ let stub_function =
| MacOS -> Stubs_MacOS.stub_function
| Linux|Diab -> Stubs_EABI.stub_function
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
match defn with
| Internal code ->
print_function oc name code
@@ -929,7 +929,7 @@ let print_fundef oc (Coq_pair(name, defn)) =
| External _ ->
()
-let record_extfun (Coq_pair(name, defn)) =
+let record_extfun (name, defn) =
match defn with
| Internal _ -> ()
| External (EF_external _) ->
@@ -967,7 +967,7 @@ let print_init_data oc name id =
else
List.iter (print_init oc) id
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
match v.gvar_init with
| [] -> ()
| _ ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 01:46:47 +0000