Commit d6344aaa authored by Armaël Guéneau's avatar Armaël Guéneau

Cleanup whitespace in generator/characteristic.ml

parent 4c204f85
......@@ -37,14 +37,14 @@ let not_in_normal_form loc s =
let external_modules = ref []
let external_modules_add name =
if not (List.mem name !external_modules)
if not (List.mem name !external_modules)
then external_modules := name::!external_modules
(* TODO: use a structure more efficient than lists *)
let external_modules_get_coqtop () =
let external_modules_get_coqtop () =
List.map (fun name -> Coqtop_require [name]) !external_modules
let external_modules_reset () =
let external_modules_reset () =
external_modules := []
......@@ -53,7 +53,7 @@ let external_modules_reset () =
(* ** Lifting of paths *)
(* Take a module name and add "_ml" suffix to it;
Moreover, insert a "Require" directive in case the module
Moreover, insert a "Require" directive in case the module
corresponds to a file (i.e. a compilation unit. *)
let lift_module_name id =
......@@ -63,34 +63,34 @@ let lift_module_name id =
coqname
(* -- old:
if Ident.persistent id
if Ident.persistent id
then (let result = name ^ "_ml" in external_modules_add result; result)
else "ML" ^ name
*)
(* -- old: if name = "OkaStream" then "CFPrim" else *)
(* Function for adding "_ml" to the modules in a path,
(* Function for adding "_ml" to the modules in a path,
including the last constant which is assumed to a module name.
For example, "Foo.Bar" becomes "Foo_ml.Bar_ml".
TODO: rename this function *)
let rec lift_full_path = function
| Pident id -> Pident (Ident.create (lift_module_name id))
| Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos)
| Papply(p1, p2) -> assert false
| Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos)
| Papply(p1, p2) -> assert false
(* Function for adding "_ml" to the modules in a path,
(* Function for adding "_ml" to the modules in a path,
but not changing the last constant in the path.
For example, "Foo.x" becomes "Foo_ml.x". *)
let lift_path = function
| Pident id -> Pident id
| Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos)
| Papply(p1, p2) -> assert false
| Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos)
| Papply(p1, p2) -> assert false
(** Translates a path into a string. A module called "Test"
(** Translates a path into a string. A module called "Test"
becomes "Test_ml". *)
let lift_full_path_name p =
......@@ -116,37 +116,37 @@ let rec fv_btyp ?(through_arrow = true) t =
| Btyp_tuple ts -> list_concat_map aux ts
| Btyp_var (s,ty) -> typvar_mark_used ty; [s]
| Btyp_poly (ss,t) -> unsupported_noloc "poly-types"
| Btyp_alias (t,s) -> s :: aux t
| Btyp_alias (t,s) -> s :: aux t
(** Translates a [btyp] into a Coq type *)
let rec lift_btyp loc t =
let aux = lift_btyp loc in
match t with
| Btyp_val ->
| Btyp_val ->
func_type
| Btyp_arrow (t1,t2) ->
| Btyp_arrow (t1,t2) ->
func_type
(* DEPRECATED
| Btyp_constr (id,[t]) when Path.name id = "array" ->
| Btyp_constr (id,[t]) when Path.name id = "array" ->
loc_type *)
| Btyp_constr (id,ts) ->
| Btyp_constr (id,ts) ->
coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
| Btyp_tuple ts ->
| Btyp_tuple ts ->
coq_prod (List.map aux ts)
| Btyp_var (s,ty) ->
| Btyp_var (s,ty) ->
typvar_mark_used ty;
Coq_var s
(* DEPRECATED
if b then unsupported loc ("non-generalizable free type variables (of the form '_a); please add a type annotation if the type is not polymorphic; if it is, then ask to get the typechecker patched for propagating the annotation. var=" ^ s);
let s = if b then "__" ^ s else s in *)
| Btyp_poly (ss,t) ->
| Btyp_poly (ss,t) ->
unsupported_noloc "poly-types"
| Btyp_alias (t1,s) ->
| Btyp_alias (t1,s) ->
let occ = fv_btyp ~through_arrow:false t1 in
if List.mem s occ
if List.mem s occ
then unsupported_noloc ("found a recursive type that is not erased by an arrow:" ^ (print_out_type t));
aux t1
aux t1
(* TEMPORARILY DEPRECATED
......@@ -156,11 +156,11 @@ let rec lift_btyp loc t =
| Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" ->
loc_type
| Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
aux t
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
| Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
aux t
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
Coq_app (Coq_var "list", aux t)
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
Coq_app (Coq_var "list", aux t)
*)
(* REMARK: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)
......@@ -169,7 +169,7 @@ let rec lift_btyp loc t =
(** Translates a Caml type into a Coq type *)
let lift_typ_exp loc ty =
lift_btyp loc (btyp_of_typ_exp ty)
lift_btyp loc (btyp_of_typ_exp ty)
(** Translates a Caml type scheme into a Coq type *)
......@@ -196,7 +196,7 @@ let coq_typ_pat loc p =
let rec path_decompose = function
Pident id -> ("", Ident.name id)
| Pdot(p, s, pos) ->
| Pdot(p, s, pos) ->
let (f,r) = path_decompose p in
(f ^ r ^ ".", s)
| Papply(p1, p2) -> unsupported_noloc "application in paths"
......@@ -204,9 +204,9 @@ let rec path_decompose = function
(** Extracts a record path_name / path from a type *)
let get_record_decomposed_name_for_exp e =
let b = btyp_of_typ_exp (e.exp_type) in
match b with
let get_record_decomposed_name_for_exp e =
let b = btyp_of_typ_exp (e.exp_type) in
match b with
| Btyp_constr (p,_) -> path_decompose (lift_path p)
| _ -> failwith "illegal argument for get_record_decomposed_name_for_exp"
......@@ -219,7 +219,7 @@ let get_record_decomposed_name_for_exp e =
let typ_arity_var env x =
match x with
| Path.Pident id ->
| Path.Pident id ->
begin try Ident.find_same id env
with Not_found -> 0 end
| _ -> 0
......@@ -234,15 +234,15 @@ let typ_arity_constr c =
(** Translate a Caml data constructor into a Coq expression *)
(* DEPRECATED: attempt to type the constructor is problematic,
because the type [ty] might not have a type constructor
because the type [ty] might not have a type constructor
that is the one from the definition of the constructor. E.g.
type 'a t = A of 'a
type 'a mylist = 'a t list
type 'a mylist = 'a t list
let empty : 'a mylist = [] ---> this is not 'a list.
let coq_of_constructor_DEPRECATED loc p c ty =
let typs =
match btyp_of_typ_exp ty with
let typs =
match btyp_of_typ_exp ty with
| Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
| _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
in
......@@ -253,12 +253,12 @@ let typ_arity_constr c =
| None -> lift_path_name p, (typ_arity_constr c)
| Some (coq_name,arity) -> coq_name, arity
in
if typs = []
if typs = []
then coq_var coq_name
else coq_apps (coq_var_at coq_name) typs
(* DEPRECATED: coq_app_var_wilds coq_name arity *)
| Tpat_construct (path, c, ps) ->
| Tpat_construct (path, c, ps) ->
coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
| Texp_construct (p, c, es) ->
coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)
......@@ -301,26 +301,26 @@ let rec pattern_variables p : typed_vars = (* ignores aliases *)
(** Translate a Caml pattern into a Coq expression, and
ignores the aliases found in the pattern *)
let rec lift_pat ?(through_aliases=true) p : coq =
let rec lift_pat ?(through_aliases=true) p : coq =
let loc = p.pat_loc in
let aux = lift_pat ~through_aliases:through_aliases in
match p.pat_desc with
| Tpat_var s ->
| Tpat_var s ->
Coq_var (var_name (Ident.name s))
| Tpat_constant (Const_int n) ->
| Tpat_constant (Const_int n) ->
Coq_int n
| Tpat_tuple l ->
| Tpat_tuple l ->
Coq_tuple (List.map aux l)
| Tpat_construct (path, c, ps) ->
| Tpat_construct (path, c, ps) ->
coq_of_constructor loc path c (List.map aux ps) p.pat_type
| Tpat_alias (p, ak) ->
| Tpat_alias (p, ak) ->
begin match ak with
| TPat_alias id ->
| TPat_alias id ->
if through_aliases then aux p else Coq_var (var_name (Ident.name id))
| TPat_constraint ty ->
let typ = lift_typ_exp loc ty.ctyp_type in
| TPat_constraint ty ->
let typ = lift_typ_exp loc ty.ctyp_type in
Coq_annot (aux p, typ)
| TPat_type pp -> aux p
| TPat_type pp -> aux p
end
| Tpat_lazy p1 ->
aux p1
......@@ -334,7 +334,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
(** Extracts the aliases from a Caml pattern, in the form of an
association list mapping variables to Coq expressions *)
let pattern_aliases p : (typed_var*coq) list =
let pattern_aliases p : (typed_var*coq) list =
let loc = p.pat_loc in
let rec aux p =
match p.pat_desc with
......@@ -342,7 +342,7 @@ let pattern_aliases p : (typed_var*coq) list =
| Tpat_constant (Const_int n) -> []
| Tpat_tuple l -> list_concat_map aux l
| Tpat_construct (p, c, ps) -> list_concat_map aux ps
| Tpat_alias (p1, ak) ->
| Tpat_alias (p1, ak) ->
begin match ak with
| TPat_alias id ->
((Ident.name id, coq_typ_pat loc p), lift_pat ~through_aliases:false p1) :: (aux p1)
......@@ -355,7 +355,7 @@ let pattern_aliases p : (typed_var*coq) list =
| Tpat_constant _ -> unsupported loc "only integer constant are supported"
| Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
| Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
| Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
| Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
in
List.rev (aux p)
......@@ -365,7 +365,7 @@ let pattern_aliases p : (typed_var*coq) list =
let register_cf x =
Coqtop_custom (sprintf "Hint Extern 1 (RegisterCF %s) => CFHeader_Provide %s." x (cf_axiom_name x))
(* DEPRECATED
(* DEPRECATED
Coqtop_register ("CFML.CFPrint.database_cf", x, cf_axiom_name x)
*)
......@@ -374,9 +374,9 @@ let register_spec x v =
(* TODO: rewrite this function by using a normalization function that returns p *)
let rec prefix_for_label typ =
match typ.desc with
| Tconstr (p, _, _) -> lift_path_name p
let rec prefix_for_label typ =
match typ.desc with
| Tconstr (p, _, _) -> lift_path_name p
| Tlink t -> prefix_for_label t
| _ -> failwith "string_of_label: type of a record should be a Tconstr or Tlink"
(*
......@@ -393,7 +393,7 @@ let rec prefix_for_label typ =
| Tpoly _ -> failwith "x12"
*)
(* DEPRECATED
(* DEPRECATED
let string_of_label_with prefix lbl =
prefix ^ "_" ^ lbl.lbl_name
......@@ -406,11 +406,11 @@ let string_of_label typ lbl =
(* ** Helper functions for primitive functions *)
let simplify_apply_args loc oargs =
List.map (function (lab, Some e, Required) -> e | _ -> unsupported loc "optional arguments") oargs
List.map (function (lab, Some e, Required) -> e | _ -> unsupported loc "optional arguments") oargs
let get_qualified_pervasives_name f =
let get_qualified_pervasives_name f =
let name = Path.name f in
if !Clflags.nopervasives
if !Clflags.nopervasives
then "Pervasives." ^ name (* unqualified name when from inside Pervasives *)
else name (* qualified name otherwise *)
......@@ -426,27 +426,27 @@ let exp_find_inlined_primitive e oargs =
in
(* _debug(); *)
begin match args with
| [n; {exp_desc = Texp_constant (Const_int m)}]
when m <> 0
&& List.mem name ["Pervasives.mod"; "Pervasives./"] ->
begin match args with
| [n; {exp_desc = Texp_constant (Const_int m)}]
when m <> 0
&& List.mem name ["Pervasives.mod"; "Pervasives./"] ->
begin match find_inlined_primitive name with
| Some (Primitive_binary_div_or_mod, coq_name) -> Some coq_name
| _ -> None
end
| [e1; e2]
when List.mem name ["Pervasives.&&"; "Pervasives.||"] ->
| [e1; e2]
when List.mem name ["Pervasives.&&"; "Pervasives.||"] ->
begin match find_inlined_primitive (Path.name f) with
| Some (Primitive_binary_lazy, coq_name) -> Some coq_name
| _ -> None
end
| [e1; e2]
when List.mem name ["Pervasives.="; "Pervasives.<>"; "Pervasives.<=";
| [e1; e2]
when List.mem name ["Pervasives.="; "Pervasives.<>"; "Pervasives.<=";
"Pervasives.>="; "Pervasives.<"; "Pervasives.>";
"Pervasives.min"; "Pervasives.max"; ] ->
let is_number =
"Pervasives.min"; "Pervasives.max"; ] ->
let is_number =
try Ctype.unify e1.exp_env e1.exp_type ((*instance*) Predef.type_int); true
with _ -> false
(*begin match btyp_of_typ_exp e1.exp_type with
......@@ -466,7 +466,7 @@ let exp_find_inlined_primitive e oargs =
| _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
end
| _ ->
| _ ->
let arity = List.length args in
begin match find_inlined_primitive name with
| Some (Primitive_unary, coq_name) when arity = 1 -> Some coq_name
......@@ -485,39 +485,39 @@ let exp_find_inlined_primitive e oargs =
(*#########################################################################*)
(* ** Lifting of values *)
(** Translate a Caml identifier into a Coq identifier, possibly
(** Translate a Caml identifier into a Coq identifier, possibly
applied to wildcards for taking type applications into account *)
let lift_exp_path env p =
match find_primitive (Path.name p) with
| None ->
| None ->
let x = lift_path_name (var_path p) in
coq_app_var_wilds x (typ_arity_var env p)
| Some y ->
Coq_var y
| Some y ->
Coq_var y
(** Translate a Caml value into a Coq value. Fails if the Coq
(** Translate a Caml value into a Coq value. Fails if the Coq
expression provided is not a value. *)
let rec lift_val env e =
let rec lift_val env e =
let loc = e.exp_loc in
let aux = lift_val env in
let fail () =
not_in_normal_form loc ("in liftval: " ^ Print_tast.string_of_expression false e) in
match e.exp_desc with
| Texp_ident (p,d) ->
lift_exp_path env p
| Texp_open (p, _) ->
| Texp_ident (p,d) ->
lift_exp_path env p
| Texp_open (p, _) ->
assert false
| Texp_constant (Const_int n) ->
Coq_int n
| Texp_constant _ ->
| Texp_constant _ ->
unsupported loc "only integer constant are supported"
| Texp_tuple el ->
| Texp_tuple el ->
Coq_tuple (List.map aux el)
| Texp_construct (p, c, es) ->
coq_of_constructor loc p c (List.map aux es) e.exp_type
| Texp_record (l, opt_init_expr) ->
| Texp_record (l, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with expression"; (* todo *)
if List.length l < 1 then failwith "record should have at least one field";
let labels = ((fun (p,li,ei) -> li) (List.hd l)).lbl_all in
......@@ -526,7 +526,7 @@ let rec lift_val env e =
Array.iteri (fun i lbli -> if lbl.lbl_name = lbli.lbl_name then args.(i) <- v) labels in
List.iter (fun (p,lbl,v) -> register_arg lbl (aux v)) l;
let constr = record_constructor_name_from_type (prefix_for_label (e.exp_type)) in
let typ_args =
let typ_args =
match btyp_of_typ_exp e.exp_type with
| Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
| _ -> failwith "record should have a type-constructor as type"
......@@ -540,14 +540,14 @@ let rec lift_val env e =
in
let args = simplify_apply_args loc oargs in
coq_apps (Coq_var f) (List.map aux args)
| Texp_lazy e ->
| Texp_lazy e ->
aux e
| Texp_constraint (e, Some ty, None) ->
| Texp_constraint (e, Some ty, None) ->
let typ = lift_typ_exp loc ty.ctyp_type in
Coq_annot (aux e, typ)
| _ -> fail()
(* --uncomment for debugging
(* --uncomment for debugging
| Texp_function _ -> not_in_normal_form loc "function"
| Texp_apply _ -> not_in_normal_form loc "apply"
| Texp_assertfalse -> not_in_normal_form loc "assert false"
......@@ -587,15 +587,15 @@ let rec lift_val env e =
(* FOR FUTURE USE *)
let counter_local_label =
let counter_local_label =
ref 0
let get_next_local_label () =
let get_next_local_label () =
incr counter_local_label;
"_m" ^ (string_of_int !counter_local_label)
let reset_local_labels() =
let reset_local_labels() =
counter_local_label := 0
let used_labels : (var list) ref =
let used_labels : (var list) ref =
ref []
let reset_used_labels () =
used_labels := []
......@@ -613,7 +613,7 @@ let cfg_extract_labels () =
(*#########################################################################*)
(* ** Helper functions for names *)
(** Takes a pattern that is expected to be reduced simply to an identifier,
(** Takes a pattern that is expected to be reduced simply to an identifier,
and returns this identifier *)
let rec pattern_ident p =
......@@ -622,7 +622,7 @@ let rec pattern_ident p =
| Tpat_alias (p1,_) -> pattern_ident p1
| _ -> failwith ("pattern_ident: the pattern is not a name: " ^ (Print_tast.string_of_pattern false p))
(** Takes a pattern that is expected to be reduced simply to an identifier,
(** Takes a pattern that is expected to be reduced simply to an identifier,
and returns the name of this identifier *)
let pattern_name p =
......@@ -660,7 +660,7 @@ let show_fvs title fvs =
(* needs to be called only after typing the body of the definition
associated with the pattern, so as to know which names are actually used. *)
let get_fvs_typ loc fvs typ =
let get_fvs_typ loc fvs typ =
let typ = lift_typ_exp loc typ in
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
(fvs, [], typ)
......@@ -672,9 +672,9 @@ let get_fvs_typ loc fvs typ =
show_fvs "fvs_typ" fvs_typ;
show_fvs "fvs" fvs;
end;
if not (list_is_included fvs_typ fvs)
if not (list_is_included fvs_typ fvs)
then failwith "fvs_typ not included in fvs for let binding";
let fvs_strict = fvs_typ in
let fvs_strict = fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(fvs_strict, fvs_others, typ)
*)
......@@ -685,7 +685,7 @@ let get_fvs_typ loc fvs typ =
(** Translate a Caml expression into its Coq characteristic formula *)
let rec cfg_exp env e =
let rec cfg_exp env e =
let loc = e.exp_loc in
let aux = cfg_exp env in
let lift e = lift_val env e in
......@@ -701,7 +701,7 @@ let rec cfg_exp env e =
(* TODO: only in purely function setting: | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with";
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift arg] in
......@@ -712,14 +712,14 @@ let rec cfg_exp env e =
(* DEPRECATED
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
let args =
let args =
try List.map (fun name -> List.assoc name named_args) fields_names
with Not_found -> failwith "some fields are missing in a record construction"
with Not_found -> failwith "some fields are missing in a record construction"
in
let tprod = coq_prod (List.map coq_typ args) in
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
......@@ -727,8 +727,8 @@ let rec cfg_exp env e =
| Texp_function (_, pat_expr_list, partial) -> not_normal ~s:"The function involved has not been lifted properly during normalization;\n check the normalized file in _output folder.\n" ()
| Texp_let(rf, fvs, pat_expr_list, body) ->
let is_let_fun =
let is_let_fun =
match (snd (List.hd pat_expr_list)).exp_desc with
| Texp_function (_,_,_) -> true
| Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
......@@ -736,7 +736,7 @@ let rec cfg_exp env e =
(* binding of functions, possibly mutually-recursive *)
if is_let_fun then begin
let env' = match rf with
let env' = match rf with
| Nonrecursive -> env
| Recursive -> env
(* --todo: add better support for local polymorphic recursion
......@@ -744,27 +744,27 @@ let rec cfg_exp env e =
| Default -> unsupported loc "Default recursion mode"
in
let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
let cf_body = cfg_exp env' body in
let cf_body = cfg_exp env' body in
add_used_label (fst (List.hd ncs));
Cf_fun (ncs, cf_body)
(* --todo: check what happens with recursive types *)
(* let-binding of a single value *)
end else begin
end else begin
if (List.length pat_expr_list <> 1) then not_normal();
let (pat,bod) = List.hd pat_expr_list in
let x = pattern_name_protect_infix pat in
(* value let-binding *)
if Typecore.is_nonexpansive bod then begin
if Typecore.is_nonexpansive bod then begin
let v =
try lift_val env bod
with Not_in_normal_form (loc2, s) ->
let v =
try lift_val env bod
with Not_in_normal_form (loc2, s) ->
raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
in
let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in
if fvs_others != []
if fvs_others != []
then unsupported loc "polymorphic let-value binding whose type-checking involves type variables that are not contained in the result type.";
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf = cfg_exp env' body in
......@@ -773,7 +773,7 @@ let rec cfg_exp env e =
(* term let-binding *)
end else begin
(* DEPRECATED
if fvs = [] then begin
(* Simple form without polymorphism *)
......@@ -783,8 +783,8 @@ let rec cfg_exp env e =
let cf2 = cfg_exp env' body in
add_used_label x;
Cf_let ((x,typ), cf1, cf2)
end else
(* General form with polymorphism *)
end else
(* General form with polymorphism *)
*)
begin
......@@ -794,12 +794,12 @@ let rec cfg_exp env e =
(* fvs_typ contains all free type variables in the type;
and thus too many w.r.t. to the ones of interest here *)
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf2 = cfg_exp env' body in
add_used_label x;
if fvs_strict = [] && fvs_others = []
if fvs_strict = [] && fvs_others = []
then Cf_let ((x,typ), cf1, cf2)
else Cf_let_poly (x, fvs_strict, fvs_others, typ, cf1, cf2)
......@@ -810,31 +810,31 @@ let rec cfg_exp env e =
not_in_normal_form loc ("(un value restriction) "
^ (Print_tast.string_of_expression false e));*)
end;
end
end
| Texp_ifthenelse (cond, ifso, Some ifnot) ->
(* old: Cf_caseif (aux cond, aux ifso, aux ifnot) *)
Cf_caseif (lift cond, aux ifso, aux ifnot)
Cf_caseif (lift cond, aux ifso, aux ifnot)
| Texp_apply (funct, oargs) ->
let args = simplify_apply_args loc oargs in
let tr = coq_typ loc e in
let ts = List.map (coq_typ loc) args in
Cf_app (ts, tr, lift funct, List.map lift args)
Cf_app (ts, tr, lift funct, List.map lift args)
| Texp_match (arg, pat_expr_list, partial) ->
let tested = lift arg in
let conclu = match partial with Partial -> Cf_fail | Total -> Cf_done in
let cfg_case (pat,body) acc =
let whenopt, cfbody =
match body.exp_desc with
let whenopt, cfbody =
match body.exp_desc with
| Texp_when (econd, ebody) ->
let w =
try lift_val env econd
with Not_in_normal_form (loc2, s) ->
let w =
try lift_val env econd
with Not_in_normal_form (loc2, s) ->
raise (Not_in_normal_form (loc2, s ^ " (Only total expressions are allowed in when clauses)"))
in
Some w, aux ebody
......@@ -845,58 +845,58 @@ let rec cfg_exp env e =
add_used_label label;
Cf_match (label, List.length pat_expr_list, List.fold_right cfg_case pat_expr_list conclu)
| Texp_assert e ->
| Texp_assert e ->
Cf_assert (aux e)
| Texp_assertfalse ->
| Texp_assertfalse ->
Cf_fail
| Texp_lazy e ->
| Texp_lazy e ->
aux e
| Texp_sequence(expr1, expr2) ->
| Texp_sequence(expr1, expr2) ->
Cf_seq (aux expr1, aux expr2)
| Texp_while(cond, body) ->
| Texp_while(cond, body) ->
Cf_while (aux cond, aux body)
| Texp_for(param, low, high, caml_dir, body) ->
let dir =
| Texp_for(param, low, high, caml_dir, body) ->
let dir =
match caml_dir with
| Upto -> For_loop_up
| Downto -> For_loop_down
in
Cf_for (dir, Ident.name param, lift low, lift high, aux body)
| Texp_array args ->
| Texp_array args ->
let arg = coq_list (List.map lift args) in
let targ = (* ['a], obtained by extraction from ['a array]. *)
let targ = (* ['a], obtained by extraction from ['a array]. *)
match btyp_of_typ_exp e.exp_type with
| Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp loc t
| _ -> failwith "Texp_array should always have type ['a array]"
in
let ts = coq_apps (Coq_var "Coq.Init.Datatypes.list") [targ] in
let tr = coq_typ loc e in (* 'a array *)
let func = Coq_var "STDLIB.Array_ml.of_list" in
let func = Coq_var "STDLIB.Array_ml.of_list" in
Cf_app ([ts], tr, func, [arg])
| Texp_field (arg, p, lbl) ->
let tr = coq_typ loc e in
| Texp_field (arg, p, lbl) ->
let tr = coq_typ loc e in
let ts = coq_typ loc arg in (* todo: check it is always 'loc' *)
let func = Coq_var "CFML.CFApp.record_get" in
let field = Coq_var (record_field_name lbl.lbl_name) in
Cf_app ([ts; coq_nat], tr, func, [lift arg; field])
Cf_app ([ts; coq_nat], tr, func, [lift arg; field])
(* DEPRECATED
let func = Coq_var (record_field_get_name lbl.lbl_name) in
Cf_app ([ts], tr, func, [lift arg])
Cf_app ([ts], tr, func, [lift arg])
*)
| Texp_setfield(arg, p, lbl, newval) ->
| Texp_setfield(arg, p, lbl, newval) ->