From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/nativecode.ml | 2117 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2117 insertions(+) create mode 100644 kernel/nativecode.ml (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml new file mode 100644 index 00000000..1a4a4b54 --- /dev/null +++ b/kernel/nativecode.ml @@ -0,0 +1,2117 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2 + | Gconstruct (s1, c1), Gconstruct (s2, c2) -> + String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2 + | Gconstant (s1, c1), Gconstant (s2, c2) -> + String.equal s1 s2 && Univ.eq_puniverses Constant.equal c1 c2 + | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 + | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 + | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 + | Gpred (Some l1, i1), Gpred (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 + | Gfixtype (None, i1), Gfixtype (None, i2) -> Int.equal i1 i2 + | Gfixtype (Some l1, i1), Gfixtype (Some l2, i2) -> + Int.equal i1 i2 && Label.equal l1 l2 + | Gnorm (None, i1), Gnorm (None, i2) -> Int.equal i1 i2 + | Gnorm (Some l1, i1), Gnorm (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 + | Gnormtbl (None, i1), Gnormtbl (None, i2) -> Int.equal i1 i2 + | Gnormtbl (Some l1, i1), Gnormtbl (Some l2, i2) -> + Int.equal i1 i2 && Label.equal l1 l2 + | Ginternal s1, Ginternal s2 -> String.equal s1 s2 + | Grel i1, Grel i2 -> Int.equal i1 i2 + | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 + | _ -> false + +open Hashset.Combine + +let gname_hash gn = match gn with +| Gind (s, (ind,u)) -> + combinesmall 1 (combine3 (String.hash s) (ind_hash ind) (Univ.Instance.hash u)) +| Gconstruct (s, (c,u)) -> + combinesmall 2 (combine3 (String.hash s) (constructor_hash c) (Univ.Instance.hash u)) +| Gconstant (s, (c,u)) -> + combinesmall 3 (combine3 (String.hash s) (Constant.hash c) (Univ.Instance.hash u)) +| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i)) +| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i)) +| Ginternal s -> combinesmall 9 (String.hash s) +| Grel i -> combinesmall 10 (Int.hash i) +| Gnamed id -> combinesmall 11 (Id.hash id) +| Gproj (s, p) -> combinesmall 12 (combine (String.hash s) (Constant.hash p)) + +let case_ctr = ref (-1) + +let reset_gcase () = case_ctr := -1 + +let fresh_gcase l = + incr case_ctr; + Gcase (l,!case_ctr) + +let pred_ctr = ref (-1) + +let reset_gpred () = pred_ctr := -1 + +let fresh_gpred l = + incr pred_ctr; + Gpred (l,!pred_ctr) + +let fixtype_ctr = ref (-1) + +let reset_gfixtype () = fixtype_ctr := -1 + +let fresh_gfixtype l = + incr fixtype_ctr; + Gfixtype (l,!fixtype_ctr) + +let norm_ctr = ref (-1) + +let reset_norm () = norm_ctr := -1 + +let fresh_gnorm l = + incr norm_ctr; + Gnorm (l,!norm_ctr) + +let normtbl_ctr = ref (-1) + +let reset_normtbl () = normtbl_ctr := -1 + +let fresh_gnormtbl l = + incr normtbl_ctr; + Gnormtbl (l,!normtbl_ctr) + +(** Symbols (pre-computed values) **) + +type symbol = + | SymbValue of Nativevalues.t + | SymbSort of sorts + | SymbName of name + | SymbConst of constant + | SymbMatch of annot_sw + | SymbInd of inductive + | SymbMeta of metavariable + | SymbEvar of existential + | SymbLevel of Univ.Level.t + +let dummy_symb = SymbValue (dummy_value ()) + +let eq_symbol sy1 sy2 = + match sy1, sy2 with + | SymbValue v1, SymbValue v2 -> Pervasives.(=) v1 v2 (** FIXME: how is this even valid? *) + | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2 + | SymbName n1, SymbName n2 -> Name.equal n1 n2 + | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2 + | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2 + | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 + | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 + | SymbEvar (evk1,args1), SymbEvar (evk2,args2) -> + Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2 + | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 + | _, _ -> false + +let hash_symbol symb = + match symb with + | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *) + | SymbSort s -> combinesmall 2 (Sorts.hash s) + | SymbName name -> combinesmall 3 (Name.hash name) + | SymbConst c -> combinesmall 4 (Constant.hash c) + | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) + | SymbInd ind -> combinesmall 6 (ind_hash ind) + | SymbMeta m -> combinesmall 7 m + | SymbEvar (evk,args) -> + let evh = Evar.hash evk in + let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in + combinesmall 8 hl + | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) + +module HashedTypeSymbol = struct + type t = symbol + let equal = eq_symbol + let hash = hash_symbol +end + +module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol) + +let symb_tbl = HashtblSymbol.create 211 + +let clear_symb_tbl () = HashtblSymbol.clear symb_tbl + +let get_value tbl i = + match tbl.(i) with + | SymbValue v -> v + | _ -> anomaly (Pp.str "get_value failed") + +let get_sort tbl i = + match tbl.(i) with + | SymbSort s -> s + | _ -> anomaly (Pp.str "get_sort failed") + +let get_name tbl i = + match tbl.(i) with + | SymbName id -> id + | _ -> anomaly (Pp.str "get_name failed") + +let get_const tbl i = + match tbl.(i) with + | SymbConst kn -> kn + | _ -> anomaly (Pp.str "get_const failed") + +let get_match tbl i = + match tbl.(i) with + | SymbMatch case_info -> case_info + | _ -> anomaly (Pp.str "get_match failed") + +let get_ind tbl i = + match tbl.(i) with + | SymbInd ind -> ind + | _ -> anomaly (Pp.str "get_ind failed") + +let get_meta tbl i = + match tbl.(i) with + | SymbMeta m -> m + | _ -> anomaly (Pp.str "get_meta failed") + +let get_evar tbl i = + match tbl.(i) with + | SymbEvar ev -> ev + | _ -> anomaly (Pp.str "get_evar failed") + +let get_level tbl i = + match tbl.(i) with + | SymbLevel u -> u + | _ -> anomaly (Pp.str "get_level failed") + +let push_symbol x = + try HashtblSymbol.find symb_tbl x + with Not_found -> + let i = HashtblSymbol.length symb_tbl in + HashtblSymbol.add symb_tbl x i; i + +let symbols_tbl_name = Ginternal "symbols_tbl" + +let get_symbols_tbl () = + let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in + HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl + +(** Lambda to Mllambda **) + +type primitive = + | Mk_prod + | Mk_sort + | Mk_ind + | Mk_const + | Mk_sw + | Mk_fix of rec_pos * int + | Mk_cofix of int + | Mk_rel of int + | Mk_var of identifier + | Mk_proj + | Is_accu + | Is_int + | Cast_accu + | Upd_cofix + | Force_cofix + | Mk_uint + | Mk_int + | Mk_bool + | Val_to_int + | Mk_I31_accu + | Decomp_uint + | Mk_meta + | Mk_evar + | MLand + | MLle + | MLlt + | MLinteq + | MLlsl + | MLlsr + | MLland + | MLlor + | MLlxor + | MLadd + | MLsub + | MLmul + | MLmagic + | MLarrayget + | Mk_empty_instance + | Coq_primitive of Primitives.t * (prefix * constant) option + +let eq_primitive p1 p2 = + match p1, p2 with + | Mk_prod, Mk_prod -> true + | Mk_sort, Mk_sort -> true + | Mk_ind, Mk_ind -> true + | Mk_const, Mk_const -> true + | Mk_sw, Mk_sw -> true + | Mk_fix (rp1, i1), Mk_fix (rp2, i2) -> Int.equal i1 i2 && eq_rec_pos rp1 rp2 + | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2 + | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2 + | Mk_var id1, Mk_var id2 -> Id.equal id1 id2 + | Is_accu, Is_accu -> true + | Cast_accu, Cast_accu -> true + | Upd_cofix, Upd_cofix -> true + | Force_cofix, Force_cofix -> true + | Mk_meta, Mk_meta -> true + | Mk_evar, Mk_evar -> true + | Mk_proj, Mk_proj -> true + | MLarrayget, MLarrayget -> true + + | _ -> false + +let primitive_hash = function + | Mk_prod -> 1 + | Mk_sort -> 2 + | Mk_ind -> 3 + | Mk_const -> 4 + | Mk_sw -> 5 + | Mk_fix (r, i) -> + let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in + combinesmall 6 (combine h (Int.hash i)) + | Mk_cofix i -> + combinesmall 7 (Int.hash i) + | Mk_rel i -> + combinesmall 8 (Int.hash i) + | Mk_var id -> + combinesmall 9 (Id.hash id) + | Is_accu -> 10 + | Is_int -> 11 + | Cast_accu -> 12 + | Upd_cofix -> 13 + | Force_cofix -> 14 + | Mk_uint -> 15 + | Mk_int -> 16 + | Mk_bool -> 17 + | Val_to_int -> 18 + | Mk_I31_accu -> 19 + | Decomp_uint -> 20 + | Mk_meta -> 21 + | Mk_evar -> 22 + | MLand -> 23 + | MLle -> 24 + | MLlt -> 25 + | MLinteq -> 26 + | MLlsl -> 27 + | MLlsr -> 28 + | MLland -> 29 + | MLlor -> 30 + | MLlxor -> 31 + | MLadd -> 32 + | MLsub -> 33 + | MLmul -> 34 + | MLmagic -> 35 + | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim) + | Coq_primitive (prim, Some (prefix,kn)) -> + combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim)) + | Mk_proj -> 38 + | MLarrayget -> 39 + | Mk_empty_instance -> 40 + +type mllambda = + | MLlocal of lname + | MLglobal of gname + | MLprimitive of primitive + | MLlam of lname array * mllambda + | MLletrec of (lname * lname array * mllambda) array * mllambda + | MLlet of lname * mllambda * mllambda + | MLapp of mllambda * mllambda array + | MLif of mllambda * mllambda * mllambda + | MLmatch of annot_sw * mllambda * mllambda * mllam_branches + (* argument, prefix, accu branch, branches *) + | MLconstruct of string * constructor * mllambda array + (* prefix, constructor name, arguments *) + | MLint of int + | MLuint of Uint31.t + | MLsetref of string * mllambda + | MLsequence of mllambda * mllambda + | MLarray of mllambda array + +and mllam_branches = ((constructor * lname option array) list * mllambda) array + +let push_lnames n env lns = + snd (Array.fold_left (fun (i,r) x -> (i+1, LNmap.add x i r)) (n,env) lns) + +let opush_lnames n env lns = + let oadd x i r = match x with Some ln -> LNmap.add ln i r | None -> r in + snd (Array.fold_left (fun (i,r) x -> (i+1, oadd x i r)) (n,env) lns) + +(* Alpha-equivalence on mllambda *) +(* eq_mllambda gn1 gn2 n env1 env2 t1 t2 tests if t1 = t2 modulo gn1 = gn2 *) +let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = + match t1, t2 with + | MLlocal ln1, MLlocal ln2 -> + Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2) + | MLglobal gn1', MLglobal gn2' -> + eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2') + | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2 + | MLlam (lns1, ml1), MLlam (lns2, ml2) -> + Int.equal (Array.length lns1) (Array.length lns2) && + let env1 = push_lnames n env1 lns1 in + let env2 = push_lnames n env2 lns2 in + eq_mllambda gn1 gn2 (n+Array.length lns1) env1 env2 ml1 ml2 + | MLletrec (defs1, body1), MLletrec (defs2, body2) -> + Int.equal (Array.length defs1) (Array.length defs2) && + let lns1 = Array.map (fun (x,_,_) -> x) defs1 in + let lns2 = Array.map (fun (x,_,_) -> x) defs2 in + let env1 = push_lnames n env1 lns1 in + let env2 = push_lnames n env2 lns2 in + let n = n + Array.length defs1 in + eq_letrec gn1 gn2 n env1 env2 defs1 defs2 && + eq_mllambda gn1 gn2 n env1 env2 body1 body2 + | MLlet (ln1, def1, body1), MLlet (ln2, def2, body2) -> + eq_mllambda gn1 gn2 n env1 env2 def1 def2 && + let env1 = LNmap.add ln1 n env1 in + let env2 = LNmap.add ln2 n env2 in + eq_mllambda gn1 gn2 (n+1) env1 env2 body1 body2 + | MLapp (ml1, args1), MLapp (ml2, args2) -> + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 && + Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2 + | MLif (cond1,br1,br'1), MLif (cond2,br2,br'2) -> + eq_mllambda gn1 gn2 n env1 env2 cond1 cond2 && + eq_mllambda gn1 gn2 n env1 env2 br1 br2 && + eq_mllambda gn1 gn2 n env1 env2 br'1 br'2 + | MLmatch (annot1, c1, accu1, br1), MLmatch (annot2, c2, accu2, br2) -> + eq_annot_sw annot1 annot2 && + eq_mllambda gn1 gn2 n env1 env2 c1 c2 && + eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 && + eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 + | MLconstruct (pf1, cs1, args1), MLconstruct (pf2, cs2, args2) -> + String.equal pf1 pf2 && + eq_constructor cs1 cs2 && + Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2 + | MLint i1, MLint i2 -> + Int.equal i1 i2 + | MLuint i1, MLuint i2 -> + Uint31.equal i1 i2 + | MLsetref (id1, ml1), MLsetref (id2, ml2) -> + String.equal id1 id2 && + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 + | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) -> + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 && + eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2 + | MLarray arr1, MLarray arr2 -> + Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 + + | _, _ -> false + +and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = + let eq_def (_,args1,ml1) (_,args2,ml2) = + Int.equal (Array.length args1) (Array.length args2) && + let env1 = push_lnames n env1 args1 in + let env2 = push_lnames n env2 args2 in + eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 ml1 ml2 + in + Array.equal eq_def defs1 defs2 + +(* we require here that patterns have the same order, which may be too strong *) +and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 = + let eq_cargs (cs1, args1) (cs2, args2) body1 body2 = + Int.equal (Array.length args1) (Array.length args2) && + eq_constructor cs1 cs2 && + let env1 = opush_lnames n env1 args1 in + let env2 = opush_lnames n env2 args2 in + eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 body1 body2 + in + let eq_branch (ptl1,body1) (ptl2,body2) = + List.equal (fun pt1 pt2 -> eq_cargs pt1 pt2 body1 body2) ptl1 ptl2 + in + Array.equal eq_branch br1 br2 + +(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *) +let rec hash_mllambda gn n env t = + match t with + | MLlocal ln -> combinesmall 1 (LNmap.find ln env) + | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else gname_hash gn') + | MLprimitive prim -> combinesmall 3 (primitive_hash prim) + | MLlam (lns, ml) -> + let env = push_lnames n env lns in + combinesmall 4 (combine (Array.length lns) (hash_mllambda gn (n+1) env ml)) + | MLletrec (defs, body) -> + let lns = Array.map (fun (x,_,_) -> x) defs in + let env = push_lnames n env lns in + let n = n + Array.length defs in + let h = combine (hash_mllambda gn n env body) (Array.length defs) in + combinesmall 5 (hash_mllambda_letrec gn n env h defs) + | MLlet (ln, def, body) -> + let hdef = hash_mllambda gn n env def in + let env = LNmap.add ln n env in + combinesmall 6 (combine hdef (hash_mllambda gn (n+1) env body)) + | MLapp (ml, args) -> + let h = hash_mllambda gn n env ml in + combinesmall 7 (hash_mllambda_array gn n env h args) + | MLif (cond,br,br') -> + let hcond = hash_mllambda gn n env cond in + let hbr = hash_mllambda gn n env br in + let hbr' = hash_mllambda gn n env br' in + combinesmall 8 (combine3 hcond hbr hbr') + | MLmatch (annot, c, accu, br) -> + let hannot = hash_annot_sw annot in + let hc = hash_mllambda gn n env c in + let haccu = hash_mllambda gn n env accu in + combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br) + | MLconstruct (pf, cs, args) -> + let hpf = String.hash pf in + let hcs = constructor_hash cs in + combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args) + | MLint i -> + combinesmall 11 i + | MLuint i -> + combinesmall 12 (Uint31.to_int i) + | MLsetref (id, ml) -> + let hid = String.hash id in + let hml = hash_mllambda gn n env ml in + combinesmall 13 (combine hid hml) + | MLsequence (ml, ml') -> + let hml = hash_mllambda gn n env ml in + let hml' = hash_mllambda gn n env ml' in + combinesmall 14 (combine hml hml') + | MLarray arr -> + combinesmall 15 (hash_mllambda_array gn n env 1 arr) + +and hash_mllambda_letrec gn n env init defs = + let hash_def (_,args,ml) = + let env = push_lnames n env args in + let nargs = Array.length args in + combine nargs (hash_mllambda gn (n + nargs) env ml) + in + Array.fold_left (fun acc t -> combine (hash_def t) acc) init defs + +and hash_mllambda_array gn n env init arr = + Array.fold_left (fun acc t -> combine (hash_mllambda gn n env t) acc) init arr + +and hash_mllam_branches gn n env init br = + let hash_cargs (cs, args) body = + let nargs = Array.length args in + let hcs = constructor_hash cs in + let env = opush_lnames n env args in + let hbody = hash_mllambda gn (n + nargs) env body in + combine3 nargs hcs hbody + in + let hash_branch acc (ptl,body) = + List.fold_left (fun acc t -> combine (hash_cargs t body) acc) acc ptl + in + Array.fold_left hash_branch init br + +let fv_lam l = + let rec aux l bind fv = + match l with + | MLlocal l -> + if LNset.mem l bind then fv else LNset.add l fv + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> fv + | MLlam (ln,body) -> + let bind = Array.fold_right LNset.add ln bind in + aux body bind fv + | MLletrec(bodies,def) -> + let bind = + Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in + let fv_body (_,ln,body) fv = + let bind = Array.fold_right LNset.add ln bind in + aux body bind fv in + Array.fold_right fv_body bodies (aux def bind fv) + | MLlet(l,def,body) -> + aux body (LNset.add l bind) (aux def bind fv) + | MLapp(f,args) -> + let fv_arg arg fv = aux arg bind fv in + Array.fold_right fv_arg args (aux f bind fv) + | MLif(t,b1,b2) -> + aux t bind (aux b1 bind (aux b2 bind fv)) + | MLmatch(_,a,p,bs) -> + let fv = aux a bind (aux p bind fv) in + let fv_bs (cargs, body) fv = + let bind = + List.fold_right (fun (_,args) bind -> + Array.fold_right + (fun o bind -> match o with + | Some l -> LNset.add l bind + | _ -> bind) args bind) + cargs bind in + aux body bind fv in + Array.fold_right fv_bs bs fv + (* argument, accu branch, branches *) + | MLconstruct (_,_,p) -> + Array.fold_right (fun a fv -> aux a bind fv) p fv + | MLsetref(_,l) -> aux l bind fv + | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) + | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + in + aux l LNset.empty LNset.empty + + +let mkMLlam params body = + if Array.is_empty params then body + else + match body with + | MLlam (params', body) -> MLlam(Array.append params params', body) + | _ -> MLlam(params,body) + +let mkMLapp f args = + if Array.is_empty args then f + else + match f with + | MLapp(f,args') -> MLapp(f,Array.append args' args) + | _ -> MLapp(f,args) + +let empty_params = [||] + +let decompose_MLlam c = + match c with + | MLlam(ids,c) -> ids,c + | _ -> empty_params,c + +(*s Global declaration *) +type global = +(* | Gtblname of gname * identifier array *) + | Gtblnorm of gname * lname array * mllambda array + | Gtblfixtype of gname * lname array * mllambda array + | Glet of gname * mllambda + | Gletcase of + gname * lname array * annot_sw * mllambda * mllambda * mllam_branches + | Gopen of string + | Gtype of inductive * int array + (* ind name, arities of constructors *) + | Gcomment of string + +(* Alpha-equivalence on globals *) +let eq_global g1 g2 = + match g1, g2 with + | Gtblnorm (gn1,lns1,mls1), Gtblnorm (gn2,lns2,mls2) + | Gtblfixtype (gn1,lns1,mls1), Gtblfixtype (gn2,lns2,mls2) -> + Int.equal (Array.length lns1) (Array.length lns2) && + Int.equal (Array.length mls1) (Array.length mls2) && + let env1 = push_lnames 0 LNmap.empty lns1 in + let env2 = push_lnames 0 LNmap.empty lns2 in + Array.for_all2 (eq_mllambda gn1 gn2 (Array.length lns1) env1 env2) mls1 mls2 + | Glet (gn1, def1), Glet (gn2, def2) -> + eq_mllambda gn1 gn2 0 LNmap.empty LNmap.empty def1 def2 + | Gletcase (gn1,lns1,annot1,c1,accu1,br1), + Gletcase (gn2,lns2,annot2,c2,accu2,br2) -> + Int.equal (Array.length lns1) (Array.length lns2) && + let env1 = push_lnames 0 LNmap.empty lns1 in + let env2 = push_lnames 0 LNmap.empty lns2 in + let t1 = MLmatch (annot1,c1,accu1,br1) in + let t2 = MLmatch (annot2,c2,accu2,br2) in + eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2 + | Gopen s1, Gopen s2 -> String.equal s1 s2 + | Gtype (ind1, arr1), Gtype (ind2, arr2) -> + eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2 + | Gcomment s1, Gcomment s2 -> String.equal s1 s2 + | _, _ -> false + +let hash_global g = + match g with + | Gtblnorm (gn,lns,mls) -> + let nlns = Array.length lns in + let nmls = Array.length mls in + let env = push_lnames 0 LNmap.empty lns in + let hmls = hash_mllambda_array gn nlns env (combine nlns nmls) mls in + combinesmall 1 hmls + | Gtblfixtype (gn,lns,mls) -> + let nlns = Array.length lns in + let nmls = Array.length mls in + let env = push_lnames 0 LNmap.empty lns in + let hmls = hash_mllambda_array gn nlns env (combine nlns nmls) mls in + combinesmall 2 hmls + | Glet (gn, def) -> + combinesmall 3 (hash_mllambda gn 0 LNmap.empty def) + | Gletcase (gn,lns,annot,c,accu,br) -> + let nlns = Array.length lns in + let env = push_lnames 0 LNmap.empty lns in + let t = MLmatch (annot,c,accu,br) in + combinesmall 4 (combine nlns (hash_mllambda gn nlns env t)) + | Gopen s -> combinesmall 5 (String.hash s) + | Gtype (ind, arr) -> + combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr)) + | Gcomment s -> combinesmall 7 (String.hash s) + +let global_stack = ref ([] : global list) + +module HashedTypeGlobal = struct + type t = global + let equal = eq_global + let hash = hash_global +end + +module HashtblGlobal = Hashtbl.Make(HashedTypeGlobal) + +let global_tbl = HashtblGlobal.create 19991 + +let clear_global_tbl () = HashtblGlobal.clear global_tbl + +let push_global gn t = + try HashtblGlobal.find global_tbl t + with Not_found -> + (global_stack := t :: !global_stack; + HashtblGlobal.add global_tbl t gn; gn) + +let push_global_let gn body = + push_global gn (Glet (gn,body)) + +let push_global_fixtype gn params body = + push_global gn (Gtblfixtype (gn,params,body)) + +let push_global_norm gn params body = + push_global gn (Gtblnorm (gn, params, body)) + +let push_global_case gn params annot a accu bs = + push_global gn (Gletcase (gn, params, annot, a, accu, bs)) + +(*s Compilation environment *) + +type env = + { env_rel : mllambda list; (* (MLlocal lname) list *) + env_bound : int; (* length of env_rel *) + (* free variables *) + env_urel : (int * mllambda) list ref; (* list of unbound rel *) + env_named : (identifier * mllambda) list ref; + env_univ : lname option} + +let empty_env univ () = + { env_rel = []; + env_bound = 0; + env_urel = ref []; + env_named = ref []; + env_univ = univ + } + +let push_rel env id = + let local = fresh_lname id in + local, { env with + env_rel = MLlocal local :: env.env_rel; + env_bound = env.env_bound + 1 + } + +let push_rels env ids = + let lnames, env_rel = + Array.fold_left (fun (names,env_rel) id -> + let local = fresh_lname id in + (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in + Array.of_list (List.rev lnames), { env with + env_rel = env_rel; + env_bound = env.env_bound + Array.length ids + } + +let get_rel env id i = + if i <= env.env_bound then + List.nth env.env_rel (i-1) + else + let i = i - env.env_bound in + try Int.List.assoc i !(env.env_urel) + with Not_found -> + let local = MLlocal (fresh_lname id) in + env.env_urel := (i,local) :: !(env.env_urel); + local + +let get_var env id = + try Id.List.assoc id !(env.env_named) + with Not_found -> + let local = MLlocal (fresh_lname (Name id)) in + env.env_named := (id, local)::!(env.env_named); + local + +let fresh_univ () = + fresh_lname (Name (Id.of_string "univ")) + +(*s Traduction of lambda to mllambda *) + +let get_prod_name codom = + match codom with + | MLlam(ids,_) -> ids.(0).lname + | _ -> assert false + +let get_lname (_,l) = + match l with + | MLlocal id -> id + | _ -> invalid_arg "Nativecode.get_lname" + +(* Collects free variables from env in an array of local names *) +let fv_params env = + let fvn, fvr = !(env.env_named), !(env.env_urel) in + let size = List.length fvn + List.length fvr in + let start,params = match env.env_univ with + | None -> 0, Array.make size dummy_lname + | Some u -> 1, let t = Array.make (size + 1) dummy_lname in t.(0) <- u; t + in + if Array.is_empty params then empty_params + else begin + let fvn = ref fvn in + let i = ref start in + while not (List.is_empty !fvn) do + params.(!i) <- get_lname (List.hd !fvn); + fvn := List.tl !fvn; + incr i + done; + let fvr = ref fvr in + while not (List.is_empty !fvr) do + params.(!i) <- get_lname (List.hd !fvr); + fvr := List.tl !fvr; + incr i + done; + params + end + +let generalize_fv env body = + mkMLlam (fv_params env) body + +let empty_args = [||] + +let fv_args env fvn fvr = + let size = List.length fvn + List.length fvr in + let start,args = match env.env_univ with + | None -> 0, Array.make size (MLint 0) + | Some u -> 1, let t = Array.make (size + 1) (MLint 0) in t.(0) <- MLlocal u; t + in + if Array.is_empty args then empty_args + else + begin + let fvn = ref fvn in + let i = ref start in + while not (List.is_empty !fvn) do + args.(!i) <- get_var env (fst (List.hd !fvn)); + fvn := List.tl !fvn; + incr i + done; + let fvr = ref fvr in + while not (List.is_empty !fvr) do + let (k,_ as kml) = List.hd !fvr in + let n = get_lname kml in + args.(!i) <- get_rel env n.lname k; + fvr := List.tl !fvr; + incr i + done; + args + end + +let get_value_code i = + MLapp (MLglobal (Ginternal "get_value"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_sort_code i = + MLapp (MLglobal (Ginternal "get_sort"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_name_code i = + MLapp (MLglobal (Ginternal "get_name"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_const_code i = + MLapp (MLglobal (Ginternal "get_const"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_match_code i = + MLapp (MLglobal (Ginternal "get_match"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_ind_code i = + MLapp (MLglobal (Ginternal "get_ind"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_meta_code i = + MLapp (MLglobal (Ginternal "get_meta"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_evar_code i = + MLapp (MLglobal (Ginternal "get_evar"), + [|MLglobal symbols_tbl_name; MLint i|]) + +let get_level_code i = + MLapp (MLglobal (Ginternal "get_level"), + [|MLglobal symbols_tbl_name; MLint i|]) + +type rlist = + | Rnil + | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' +and rlist' = rlist ref + +let rm_params fv params = + Array.map (fun l -> if LNset.mem l fv then Some l else None) params + +let rec insert cargs body rl = + match !rl with + | Rnil -> + let fv = fv_lam body in + let (c,params) = cargs in + let params = rm_params fv params in + rl:= Rcons(ref [(c,params)], fv, body, ref Rnil) + | Rcons(l,fv,body',rl) -> + (** ppedrot: It seems we only want to factorize common branches. It should + not matter to do so with a subapproximation by (==). *) + if body == body' then + let (c,params) = cargs in + let params = rm_params fv params in + l := (c,params)::!l + else insert cargs body rl + +let rec to_list rl = + match !rl with + | Rnil -> [] + | Rcons(l,_,body,tl) -> (!l,body)::to_list tl + +let merge_branches t = + let newt = ref Rnil in + Array.iter (fun (c,args,body) -> insert (c,args) body newt) t; + Array.of_list (to_list newt) + + +type prim_aux = + | PAprim of string * constant * Primitives.t * prim_aux array + | PAml of mllambda + +let add_check cond args = + let aux cond a = + match a with + | PAml(MLint _) -> cond + | PAml ml -> + (* FIXME: use explicit equality function *) + if List.mem ml cond then cond else ml::cond + | _ -> cond + in + Array.fold_left aux cond args + +let extract_prim ml_of l = + let decl = ref [] in + let cond = ref [] in + let rec aux l = + match l with + | Lprim(prefix,kn,p,args) -> + let args = Array.map aux args in + cond := add_check !cond args; + PAprim(prefix,kn,p,args) + | Lrel _ | Lvar _ | Luint _ | Lval _ | Lconst _ -> PAml (ml_of l) + | _ -> + let x = fresh_lname Anonymous in + decl := (x,ml_of l)::!decl; + PAml (MLlocal x) in + let res = aux l in + (!decl, !cond, res) + +let app_prim p args = MLapp(MLprimitive p, args) + +let to_int v = + match v with + | MLapp(MLprimitive Mk_uint, t) -> + begin match t.(0) with + | MLuint i -> MLint (Uint31.to_int i) + | _ -> MLapp(MLprimitive Val_to_int, [|v|]) + end + | MLapp(MLprimitive Mk_int, t) -> t.(0) + | _ -> MLapp(MLprimitive Val_to_int, [|v|]) + +let of_int v = + match v with + | MLapp(MLprimitive Val_to_int, t) -> t.(0) + | _ -> MLapp(MLprimitive Mk_int,[|v|]) + +let compile_prim decl cond paux = +(* + let args_to_int args = + for i = 0 to Array.length args - 1 do + args.(i) <- to_int args.(i) + done; + args in + *) + let rec opt_prim_aux paux = + match paux with + | PAprim(prefix, kn, op, args) -> + let args = Array.map opt_prim_aux args in + app_prim (Coq_primitive(op,None)) args +(* + TODO: check if this inling was useful + begin match op with + | Int31lt -> + if Sys.word_size = 64 then + app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|] + else app_prim (Coq_primitive (Primitives.Int31lt,None)) args + | Int31le -> + if Sys.word_size = 64 then + app_prim Mk_bool [|(app_prim MLle (args_to_int args))|] + else app_prim (Coq_primitive (Primitives.Int31le, None)) args + | Int31lsl -> of_int (mk_lsl (args_to_int args)) + | Int31lsr -> of_int (mk_lsr (args_to_int args)) + | Int31land -> of_int (mk_land (args_to_int args)) + | Int31lor -> of_int (mk_lor (args_to_int args)) + | Int31lxor -> of_int (mk_lxor (args_to_int args)) + | Int31add -> of_int (mk_add (args_to_int args)) + | Int31sub -> of_int (mk_sub (args_to_int args)) + | Int31mul -> of_int (mk_mul (args_to_int args)) + | _ -> app_prim (Coq_primitive(op,None)) args + end *) + | PAml ml -> ml + and naive_prim_aux paux = + match paux with + | PAprim(prefix, kn, op, args) -> + app_prim (Coq_primitive(op, Some (prefix, kn))) (Array.map naive_prim_aux args) + | PAml ml -> ml in + + let compile_cond cond paux = + match cond with + | [] -> opt_prim_aux paux + | [c1] -> + MLif(app_prim Is_int [|c1|], opt_prim_aux paux, naive_prim_aux paux) + | c1::cond -> + let cond = + List.fold_left + (fun ml c -> app_prim MLland [| ml; to_int c|]) + (app_prim MLland [|to_int c1; MLint 0 |]) cond in + let cond = app_prim MLmagic [|cond|] in + MLif(cond, naive_prim_aux paux, opt_prim_aux paux) in + let add_decl decl body = + List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in + add_decl decl (compile_cond cond paux) + +let ml_of_instance instance u = + let ml_of_level l = + match Univ.Level.var_index l with + | Some i -> + let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in + mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|] + | None -> let i = push_symbol (SymbLevel l) in get_level_code i + in + let u = Univ.Instance.to_array u in + if Array.is_empty u then [||] + else let u = Array.map ml_of_level u in + [|MLapp (MLprimitive MLmagic, [|MLarray u|])|] + + let rec ml_of_lam env l t = + match t with + | Lrel(id ,i) -> get_rel env id i + | Lvar id -> get_var env id + | Lmeta(mv,ty) -> + let tyn = fresh_lname Anonymous in + let i = push_symbol (SymbMeta mv) in + MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) + | Levar(ev,ty) -> + let tyn = fresh_lname Anonymous in + let i = push_symbol (SymbEvar ev) in + MLlet(tyn, ml_of_lam env l ty, + MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn|])) + | Lprod(dom,codom) -> + let dom = ml_of_lam env l dom in + let codom = ml_of_lam env l codom in + let n = get_prod_name codom in + let i = push_symbol (SymbName n) in + MLapp(MLprimitive Mk_prod, [|get_name_code i;dom;codom|]) + | Llam(ids,body) -> + let lnames,env = push_rels env ids in + MLlam(lnames, ml_of_lam env l body) + | Llet(id,def,body) -> + let def = ml_of_lam env l def in + let lname, env = push_rel env id in + let body = ml_of_lam env l body in + MLlet(lname,def,body) + | Lapp(f,args) -> + MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args) + | Lconst (prefix,c) -> + let args = ml_of_instance env.env_univ (snd c) in + mkMLapp (MLglobal(Gconstant (prefix,c))) args + | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) + | Lprim _ -> + let decl,cond,paux = extract_prim (ml_of_lam env l) t in + compile_prim decl cond paux + | Lcase (annot,p,a,bs) -> + (* let predicate_uid fv_pred = compilation of p + let rec case_uid fv a_uid = + match a_uid with + | Accu _ => mk_sw (predicate_uid fv_pred) (case_uid fv) a_uid + | Ci argsi => compilation of branches + compile case = case_uid fv (compilation of a) *) + (* Compilation of the predicate *) + (* Remark: if we do not want to compile the predicate we + should a least compute the fv, then store the lambda representation + of the predicate (not the mllambda) *) + let env_p = empty_env env.env_univ () in + let pn = fresh_gpred l in + let mlp = ml_of_lam env_p l p in + let mlp = generalize_fv env_p mlp in + let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in + let pn = push_global_let pn mlp in + (* Compilation of the case *) + let env_c = empty_env env.env_univ () in + let a_uid = fresh_lname Anonymous in + let la_uid = MLlocal a_uid in + (* compilation of branches *) + let ml_br (c,params, body) = + let lnames, env_c = push_rels env_c params in + (c, lnames, ml_of_lam env_c l body) + in + let bs = Array.map ml_br bs in + let cn = fresh_gcase l in + (* Compilation of accu branch *) + let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in + let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in + let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in + (* remark : the call to fv_args does not add free variables in env_c *) + let i = push_symbol (SymbMatch annot) in + let accu = + MLapp(MLprimitive Mk_sw, + [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]); + pred; + cn_fv |]) in +(* let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in + let case = generalize_fv env_c body in *) + let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|]) + annot la_uid accu (merge_branches bs) + in + (* Final result *) + let arg = ml_of_lam env l a in + let force = + if annot.asw_finite then arg + else MLapp(MLprimitive Force_cofix, [|arg|]) in + mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] + | Lif(t,bt,bf) -> + MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) + | Lfix ((rec_pos,start), (ids, tt, tb)) -> + (* let type_f fvt = [| type fix |] + let norm_f1 fv f1 .. fn params1 = body1 + .. + let norm_fn fv f1 .. fn paramsn = bodyn + let norm fv f1 .. fn = + [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|] + compile fix = + let rec f1 params1 = + if is_accu rec_pos.(1) then mk_fix (type_f fvt) (norm fv) params1 + else norm_f1 fv f1 .. fn params1 + and .. and fn paramsn = + if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn + else norm_fn fv f1 .. fv paramsn in + start + *) + (* Compilation of type *) + let env_t = empty_env env.env_univ () in + let ml_t = Array.map (ml_of_lam env_t l) tt in + let params_t = fv_params env_t in + let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in + let gft = fresh_gfixtype l in + let gft = push_global_fixtype gft params_t ml_t in + let mk_type = MLapp(MLglobal gft, args_t) in + (* Compilation of norm_i *) + let ndef = Array.length ids in + let lf,env_n = push_rels (empty_env env.env_univ ()) ids in + let t_params = Array.make ndef [||] in + let t_norm_f = Array.make ndef (Gnorm (l,-1)) in + let mk_let envi (id,def) t = MLlet (id,def,t) in + let mk_lam_or_let (params,lets,env) (id,def) = + let ln,env' = push_rel env id in + match def with + | None -> (ln::params,lets,env') + | Some lam -> (params, (ln,ml_of_lam env l lam)::lets,env') + in + let ml_of_fix i body = + let varsi, bodyi = decompose_Llam_Llet body in + let paramsi,letsi,envi = + Array.fold_left mk_lam_or_let ([],[],env_n) varsi + in + let paramsi,letsi = + Array.of_list (List.rev paramsi), Array.of_list (List.rev letsi) + in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + let bodyi = Array.fold_right (mk_let envi) letsi bodyi in + mkMLlam paramsi bodyi + in + let tnorm = Array.mapi ml_of_fix tb in + let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in + let fv_params = fv_params env_n in + let fv_args' = Array.map (fun id -> MLlocal id) fv_params in + let norm_params = Array.append fv_params lf in + let t_norm_f = Array.mapi (fun i body -> + push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in + let norm = fresh_gnormtbl l in + let norm = push_global_norm norm fv_params + (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in + (* Compilation of fix *) + let fv_args = fv_args env fvn fvr in + let lf, env = push_rels env ids in + let lf_args = Array.map (fun id -> MLlocal id) lf in + let mk_norm = MLapp(MLglobal norm, fv_args) in + let mkrec i lname = + let paramsi = t_params.(i) in + let reci = MLlocal (paramsi.(rec_pos.(i))) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let body = + MLif(MLapp(MLprimitive Is_accu,[|reci|]), + mkMLapp + (MLapp(MLprimitive (Mk_fix(rec_pos,i)), + [|mk_type; mk_norm|])) + pargsi, + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi])) + in + (lname, paramsi, body) in + MLletrec(Array.mapi mkrec lf, lf_args.(start)) + | Lcofix (start, (ids, tt, tb)) -> + (* Compilation of type *) + let env_t = empty_env env.env_univ () in + let ml_t = Array.map (ml_of_lam env_t l) tt in + let params_t = fv_params env_t in + let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in + let gft = fresh_gfixtype l in + let gft = push_global_fixtype gft params_t ml_t in + let mk_type = MLapp(MLglobal gft, args_t) in + (* Compilation of norm_i *) + let ndef = Array.length ids in + let lf,env_n = push_rels (empty_env env.env_univ ()) ids in + let t_params = Array.make ndef [||] in + let t_norm_f = Array.make ndef (Gnorm (l,-1)) in + let ml_of_fix i body = + let idsi,bodyi = decompose_Llam body in + let paramsi, envi = push_rels env_n idsi in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + mkMLlam paramsi bodyi in + let tnorm = Array.mapi ml_of_fix tb in + let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in + let fv_params = fv_params env_n in + let fv_args' = Array.map (fun id -> MLlocal id) fv_params in + let norm_params = Array.append fv_params lf in + let t_norm_f = Array.mapi (fun i body -> + push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in + let norm = fresh_gnormtbl l in + let norm = push_global_norm norm fv_params + (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in + (* Compilation of fix *) + let fv_args = fv_args env fvn fvr in + let mk_norm = MLapp(MLglobal norm, fv_args) in + let lnorm = fresh_lname Anonymous in + let ltype = fresh_lname Anonymous in + let lf, env = push_rels env ids in + let lf_args = Array.map (fun id -> MLlocal id) lf in + let upd i lname cont = + let paramsi = t_params.(i) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let uniti = fresh_lname Anonymous in + let body = + MLlam(Array.append paramsi [|uniti|], + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi])) in + MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]), + cont) in + let upd = Array.fold_right_i upd lf lf_args.(start) in + let mk_let i lname cont = + MLlet(lname, + MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]), + cont) in + let init = Array.fold_right_i mk_let lf upd in + MLlet(lnorm, mk_norm, MLlet(ltype, mk_type, init)) + (* + let mkrec i lname = + let paramsi = t_params.(i) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let uniti = fresh_lname Anonymous in + let body = + MLapp( MLprimitive(Mk_cofix i), + [|mk_type;mk_norm; + MLlam([|uniti|], + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi]))|]) in + (lname, paramsi, body) in + MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) + + | Lmakeblock (prefix,(cn,u),_,args) -> + let args = Array.map (ml_of_lam env l) args in + MLconstruct(prefix,cn,args) + | Lconstruct (prefix, (cn,u)) -> + let uargs = ml_of_instance env.env_univ u in + mkMLapp (MLglobal (Gconstruct (prefix, (cn,u)))) uargs + | Luint v -> + (match v with + | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) + | UintDigits (prefix,cn,ds) -> + let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let ds = Array.map (ml_of_lam env l) ds in + let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in + MLapp(i31, ds) + | UintDecomp (prefix,cn,t) -> + let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let t = ml_of_lam env l t in + MLapp (MLprimitive Decomp_uint, [|c;t|])) + | Lval v -> + let i = push_symbol (SymbValue v) in get_value_code i + | Lsort s -> + let i = push_symbol (SymbSort s) in + let uarg = match env.env_univ with + | None -> MLarray [||] + | Some u -> MLlocal u + in + let uarg = MLapp(MLprimitive MLmagic, [|uarg|]) in + MLapp(MLprimitive Mk_sort, [|get_sort_code i; uarg|]) + | Lind (prefix, pind) -> + let uargs = ml_of_instance env.env_univ (snd pind) in + mkMLapp (MLglobal (Gind (prefix, pind))) uargs + | Llazy -> MLglobal (Ginternal "lazy") + | Lforce -> MLglobal (Ginternal "Lazy.force") + +let mllambda_of_lambda univ auxdefs l t = + let env = empty_env univ () in + global_stack := auxdefs; + let ml = ml_of_lam env l t in + let fv_rel = !(env.env_urel) in + let fv_named = !(env.env_named) in + (* build the free variables *) + let get_lname (_,t) = + match t with + | MLlocal x -> x + | _ -> assert false in + let params = + List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in + if List.is_empty params then + (!global_stack, ([],[]), ml) + (* final result : global list, fv, ml *) + else + (!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml) + +(** Code optimization **) + +(** Optimization of match and fix *) + +let can_subst l = + match l with + | MLlocal _ | MLint _ | MLuint _ | MLglobal _ -> true + | _ -> false + +let subst s l = + if LNmap.is_empty s then l + else + let rec aux l = + match l with + | MLlocal id -> (try LNmap.find id s with Not_found -> l) + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l + | MLlam(params,body) -> MLlam(params, aux body) + | MLletrec(defs,body) -> + let arec (f,params,body) = (f,params,aux body) in + MLletrec(Array.map arec defs, aux body) + | MLlet(id,def,body) -> MLlet(id,aux def, aux body) + | MLapp(f,args) -> MLapp(aux f, Array.map aux args) + | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2) + | MLmatch(annot,a,accu,bs) -> + let auxb (cargs,body) = (cargs,aux body) in + MLmatch(annot,a,aux accu, Array.map auxb bs) + | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args) + | MLsetref(s,l1) -> MLsetref(s,aux l1) + | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) + | MLarray arr -> MLarray (Array.map aux arr) + in + aux l + +let add_subst id v s = + match v with + | MLlocal id' when Int.equal id.luid id'.luid -> s + | _ -> LNmap.add id v s + +let subst_norm params args s = + let len = Array.length params in + assert (Int.equal (Array.length args) len && Array.for_all can_subst args); + let s = ref s in + for i = 0 to len - 1 do + s := add_subst params.(i) args.(i) !s + done; + !s + +let subst_case params args s = + let len = Array.length params in + assert (len > 0 && + Int.equal (Array.length args) len && + let r = ref true and i = ref 0 in + (* we test all arguments excepted the last *) + while !i < len - 1 && !r do r := can_subst args.(!i); incr i done; + !r); + let s = ref s in + for i = 0 to len - 2 do + s := add_subst params.(i) args.(i) !s + done; + !s, params.(len-1), args.(len-1) + +let empty_gdef = Int.Map.empty, Int.Map.empty +let get_norm (gnorm, _) i = Int.Map.find i gnorm +let get_case (_, gcase) i = Int.Map.find i gcase + +let all_lam n bs = + let f (_, l) = + match l with + | MLlam(params, _) -> Int.equal (Array.length params) n + | _ -> false in + Array.for_all f bs + +let commutative_cut annot a accu bs args = + let mkb (c,b) = + match b with + | MLlam(params, body) -> + (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args) + | _ -> assert false in + MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs) + +let optimize gdef l = + let rec optimize s l = + match l with + | MLlocal id -> (try LNmap.find id s with Not_found -> l) + | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ -> l + | MLlam(params,body) -> + MLlam(params, optimize s body) + | MLletrec(decls,body) -> + let opt_rec (f,params,body) = (f,params,optimize s body ) in + MLletrec(Array.map opt_rec decls, optimize s body) + | MLlet(id,def,body) -> + let def = optimize s def in + if can_subst def then optimize (add_subst id def s) body + else MLlet(id,def,optimize s body) + | MLapp(f, args) -> + let args = Array.map (optimize s) args in + begin match f with + | MLglobal (Gnorm (_,i)) -> + (try + let params,body = get_norm gdef i in + let s = subst_norm params args s in + optimize s body + with Not_found -> MLapp(optimize s f, args)) + | MLglobal (Gcase (_,i)) -> + (try + let params,body = get_case gdef i in + let s, id, arg = subst_case params args s in + if can_subst arg then optimize (add_subst id arg s) body + else MLlet(id, arg, optimize s body) + with Not_found -> MLapp(optimize s f, args)) + | _ -> + let f = optimize s f in + match f with + | MLmatch (annot,a,accu,bs) -> + if all_lam (Array.length args) bs then + commutative_cut annot a accu bs args + else MLapp(f, args) + | _ -> MLapp(f, args) + + end + | MLif(t,b1,b2) -> + let t = optimize s t in + let b1 = optimize s b1 in + let b2 = optimize s b2 in + begin match t, b2 with + | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *) + | _, _ -> MLif(t, b1, b2) + end + | MLmatch(annot,a,accu,bs) -> + let opt_b (cargs,body) = (cargs,optimize s body) in + MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs) + | MLconstruct(prefix,c,args) -> + MLconstruct(prefix,c,Array.map (optimize s) args) + | MLsetref(r,l) -> MLsetref(r, optimize s l) + | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) + | MLarray arr -> MLarray (Array.map (optimize s) arr) + in + optimize LNmap.empty l + +let optimize_stk stk = + let add_global gdef g = + match g with + | Glet (Gnorm (_,i), body) -> + let (gnorm, gcase) = gdef in + (Int.Map.add i (decompose_MLlam body) gnorm, gcase) + | Gletcase(Gcase (_,i), params, annot,a,accu,bs) -> + let (gnorm,gcase) = gdef in + (gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase) + | Gletcase _ -> assert false + | _ -> gdef in + let gdef = List.fold_left add_global empty_gdef stk in + let optimize_global g = + match g with + | Glet(Gconstant (prefix, c), body) -> + Glet(Gconstant (prefix, c), optimize gdef body) + | _ -> g in + List.map optimize_global stk + +(** Printing to ocaml **) +(* Redefine a bunch of functions in module Names to generate names + acceptable to OCaml. *) +let string_of_id s = Unicode.ascii_of_ident (string_of_id s) +let string_of_label l = Unicode.ascii_of_ident (string_of_label l) + +let string_of_dirpath = function + | [] -> "_" + | sl -> String.concat "_" (List.rev_map string_of_id sl) + +(* The first letter of the file name has to be a capital to be accepted by *) +(* OCaml as a module identifier. *) +let string_of_dirpath s = "N"^string_of_dirpath s + +let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir) + +let link_info_of_dirpath dir = + Linked (mod_uid_of_dirpath dir ^ ".") + +let string_of_name x = + match x with + | Anonymous -> "anonymous" (* assert false *) + | Name id -> string_of_id id + +let string_of_label_def l = + match l with + | None -> "" + | Some l -> string_of_label l + +(* Relativization of module paths *) +let rec list_of_mp acc = function + | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp + | MPfile dp -> + let dp = repr_dirpath dp in + string_of_dirpath dp :: acc + | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc + +let list_of_mp mp = list_of_mp [] mp + +let string_of_kn kn = + let (mp,dp,l) = repr_kn kn in + let mp = list_of_mp mp in + String.concat "_" mp ^ "_" ^ string_of_label l + +let string_of_con c = string_of_kn (user_con c) +let string_of_mind mind = string_of_kn (user_mind mind) + +let string_of_gname g = + match g with + | Gind (prefix, ((mind,i), _)) -> + Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i + | Gconstruct (prefix, (((mind, i), j), _)) -> + Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) + | Gconstant (prefix, (c,_)) -> + Format.sprintf "%sconst_%s" prefix (string_of_con c) + | Gproj (prefix, c) -> + Format.sprintf "%sproj_%s" prefix (string_of_con c) + | Gcase (l,i) -> + Format.sprintf "case_%s_%i" (string_of_label_def l) i + | Gpred (l,i) -> + Format.sprintf "pred_%s_%i" (string_of_label_def l) i + | Gfixtype (l,i) -> + Format.sprintf "fixtype_%s_%i" (string_of_label_def l) i + | Gnorm (l,i) -> + Format.sprintf "norm_%s_%i" (string_of_label_def l) i + | Ginternal s -> Format.sprintf "%s" s + | Gnormtbl (l,i) -> + Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i + | Grel i -> + Format.sprintf "rel_%i" i + | Gnamed id -> + Format.sprintf "named_%s" (string_of_id id) + +let pp_gname fmt g = + Format.fprintf fmt "%s" (string_of_gname g) + +let pp_lname fmt ln = + let s = Unicode.ascii_of_ident (string_of_name ln.lname) in + Format.fprintf fmt "x_%s_%i" s ln.luid + +let pp_ldecls fmt ids = + let len = Array.length ids in + for i = 0 to len - 1 do + Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i) + done + +let string_of_construct prefix ((mind,i),j) = + let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in + prefix ^ id + +let pp_int fmt i = + if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i + +let pp_mllam fmt l = + + let rec pp_mllam fmt l = + match l with + | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln + | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g + | MLprimitive p -> Format.fprintf fmt "@[%a@]" pp_primitive p + | MLlam(ids,body) -> + Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]" + pp_ldecls ids pp_mllam body + | MLletrec(defs, body) -> + Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs + pp_mllam body + | MLlet(id,def,body) -> + Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]" + pp_lname id pp_mllam def pp_mllam body + | MLapp(f, args) -> + Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args + | MLif(t,l1,l2) -> + Format.fprintf fmt "@[(if %a then@\n %a@\nelse@\n %a)@]" + pp_mllam t pp_mllam l1 pp_mllam l2 + | MLmatch (annot, c, accu_br, br) -> + let mind,i = annot.asw_ind in + let prefix = annot.asw_prefix in + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]" + pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br + + | MLconstruct(prefix,c,args) -> + Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" + (string_of_construct prefix c) pp_cargs args + | MLint i -> pp_int fmt i + | MLuint i -> Format.fprintf fmt "(Uint31.of_int %a)" pp_int (Uint31.to_int i) + | MLsetref (s, body) -> + Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body + | MLsequence(l1,l2) -> + Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2 + | MLarray arr -> + let len = Array.length arr in + Format.fprintf fmt "@[[|"; + if 0 < len then begin + for i = 0 to len - 2 do + Format.fprintf fmt "%a;" pp_mllam arr.(i) + done; + pp_mllam fmt arr.(len-1) + end; + Format.fprintf fmt "|]@]" + + + and pp_letrec fmt defs = + let len = Array.length defs in + let pp_one_rec i (fn, argsn, body) = + Format.fprintf fmt "%a%a =@\n %a" + pp_lname fn + pp_ldecls argsn pp_mllam body in + Format.fprintf fmt "@[let rec "; + pp_one_rec 0 defs.(0); + for i = 1 to len - 1 do + Format.fprintf fmt "@\nand "; + pp_one_rec i defs.(i) + done; + + and pp_blam fmt l = + match l with + | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *) + | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ -> + Format.fprintf fmt "(%a)" pp_mllam l + | MLconstruct(_,_,args) when Array.length args > 0 -> + Format.fprintf fmt "(%a)" pp_mllam l + | _ -> pp_mllam fmt l + + and pp_args sep fmt args = + let sep = if sep then " " else "," in + let len = Array.length args in + if len > 0 then begin + Format.fprintf fmt "%a" pp_blam args.(0); + for i = 1 to len - 1 do + Format.fprintf fmt "%s%a" sep pp_blam args.(i) + done + end + + and pp_cargs fmt args = + let len = Array.length args in + match len with + | 0 -> () + | 1 -> Format.fprintf fmt " %a" pp_blam args.(0) + | _ -> Format.fprintf fmt "(%a)" (pp_args false) args + + and pp_cparam fmt param = + match param with + | Some l -> pp_mllam fmt (MLlocal l) + | None -> Format.fprintf fmt "_" + + and pp_cparams fmt params = + let len = Array.length params in + match len with + | 0 -> () + | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0) + | _ -> + let aux fmt params = + Format.fprintf fmt "%a" pp_cparam params.(0); + for i = 1 to len - 1 do + Format.fprintf fmt ",%a" pp_cparam params.(i) + done in + Format.fprintf fmt "(%a)" aux params + + and pp_branches prefix fmt bs = + let pp_branch (cargs,body) = + let pp_c fmt (cn,args) = + Format.fprintf fmt "| %s%a " + (string_of_construct prefix cn) pp_cparams args in + let rec pp_cargs fmt cargs = + match cargs with + | [] -> () + | cargs::cargs' -> + Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in + Format.fprintf fmt "%a ->@\n %a@\n" + pp_cargs cargs pp_mllam body + in + Array.iter pp_branch bs + + and pp_primitive fmt = function + | Mk_prod -> Format.fprintf fmt "mk_prod_accu" + | Mk_sort -> Format.fprintf fmt "mk_sort_accu" + | Mk_ind -> Format.fprintf fmt "mk_ind_accu" + | Mk_const -> Format.fprintf fmt "mk_constant_accu" + | Mk_sw -> Format.fprintf fmt "mk_sw_accu" + | Mk_fix(rec_pos,start) -> + let pp_rec_pos fmt rec_pos = + Format.fprintf fmt "@[[| %i" rec_pos.(0); + for i = 1 to Array.length rec_pos - 1 do + Format.fprintf fmt "; %i" rec_pos.(i) + done; + Format.fprintf fmt " |]@]" in + Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start + | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start + | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i + | Mk_var id -> + Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) + | Mk_proj -> Format.fprintf fmt "mk_proj_accu" + | Is_accu -> Format.fprintf fmt "is_accu" + | Is_int -> Format.fprintf fmt "is_int" + | Cast_accu -> Format.fprintf fmt "cast_accu" + | Upd_cofix -> Format.fprintf fmt "upd_cofix" + | Force_cofix -> Format.fprintf fmt "force_cofix" + | Mk_uint -> Format.fprintf fmt "mk_uint" + | Mk_int -> Format.fprintf fmt "mk_int" + | Mk_bool -> Format.fprintf fmt "mk_bool" + | Val_to_int -> Format.fprintf fmt "val_to_int" + | Mk_I31_accu -> Format.fprintf fmt "mk_I31_accu" + | Decomp_uint -> Format.fprintf fmt "decomp_uint" + | Mk_meta -> Format.fprintf fmt "mk_meta_accu" + | Mk_evar -> Format.fprintf fmt "mk_evar_accu" + | MLand -> Format.fprintf fmt "(&&)" + | MLle -> Format.fprintf fmt "(<=)" + | MLlt -> Format.fprintf fmt "(<)" + | MLinteq -> Format.fprintf fmt "(==)" + | MLlsl -> Format.fprintf fmt "(lsl)" + | MLlsr -> Format.fprintf fmt "(lsr)" + | MLland -> Format.fprintf fmt "(land)" + | MLlor -> Format.fprintf fmt "(lor)" + | MLlxor -> Format.fprintf fmt "(lxor)" + | MLadd -> Format.fprintf fmt "(+)" + | MLsub -> Format.fprintf fmt "(-)" + | MLmul -> Format.fprintf fmt "( * )" + | MLmagic -> Format.fprintf fmt "Obj.magic" + | MLarrayget -> Format.fprintf fmt "Array.get" + | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" + | Coq_primitive (op,None) -> + Format.fprintf fmt "no_check_%s" (Primitives.to_string op) + | Coq_primitive (op, Some (prefix,kn)) -> + let u = Univ.Instance.empty in + Format.fprintf fmt "%s %a" (Primitives.to_string op) + pp_mllam (MLglobal (Gconstant (prefix,(kn,u)))) + in + Format.fprintf fmt "@[%a@]" pp_mllam l + +let pp_array fmt t = + let len = Array.length t in + Format.fprintf fmt "@[[|"; + for i = 0 to len - 2 do + Format.fprintf fmt "%a; " pp_mllam t.(i) + done; + if len > 0 then + Format.fprintf fmt "%a" pp_mllam t.(len - 1); + Format.fprintf fmt "|]@]" + +let pp_global fmt g = + match g with + | Glet (gn, c) -> + let ids, c = decompose_MLlam c in + Format.fprintf fmt "@[let %a%a =@\n %a@]@\n@." pp_gname gn + pp_ldecls ids + pp_mllam c + | Gopen s -> + Format.fprintf fmt "@[open %s@]@." s + | Gtype ((mind, i), lar) -> + let l = string_of_mind mind in + let rec aux s ar = + if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in + let pp_const_sig i fmt j ar = + let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in + Format.fprintf fmt " | Construct_%s_%i_%i %s@\n" l i j sig_str + in + let pp_const_sigs i fmt lar = + Format.fprintf fmt " | Accu_%s_%i of Nativevalues.t@\n" l i; + Array.iteri (pp_const_sig i fmt) lar + in + Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar + | Gtblfixtype (g, params, t) -> + Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g + pp_ldecls params pp_array t + | Gtblnorm (g, params, t) -> + Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g + pp_ldecls params pp_array t + | Gletcase(gn,params,annot,a,accu,bs) -> + Format.fprintf fmt "@[(* Hash = %i *)@\nlet rec %a %a =@\n %a@]@\n@." + (hash_global g) + pp_gname gn pp_ldecls params + pp_mllam (MLmatch(annot,a,accu,bs)) + | Gcomment s -> + Format.fprintf fmt "@[(* %s *)@]@." s + +(** Compilation of elements in environment **) +let rec compile_with_fv env sigma univ auxdefs l t = + let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda univ auxdefs l t in + if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml) + else apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml + +and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = + let get_rel_val (n,_) auxdefs = + (* + match !(lookup_rel_native_val n env) with + | NVKnone -> + *) + compile_rel env sigma univ auxdefs n +(* | NVKvalue (v,d) -> assert false *) + in + let get_named_val (id,_) auxdefs = + (* + match !(lookup_named_native_val id env) with + | NVKnone -> + *) + compile_named env sigma univ auxdefs id +(* | NVKvalue (v,d) -> assert false *) + in + let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in + let auxdefs = List.fold_right get_named_val fv_named auxdefs in + let lvl = rel_context_length env.env_rel_context in + let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in + let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in + let aux_name = fresh_lname Anonymous in + auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) + +and compile_rel env sigma univ auxdefs n = + let (_,body,_) = lookup_rel n env.env_rel_context in + let n = rel_context_length env.env_rel_context - n in + match body with + | Some t -> + let code = lambda_of_constr env sigma t in + let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in + Glet(Grel n, code)::auxdefs + | None -> + Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs + +and compile_named env sigma univ auxdefs id = + let (_,body,_) = lookup_named id env.env_named_context in + match body with + | Some t -> + let code = lambda_of_constr env sigma t in + let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in + Glet(Gnamed id, code)::auxdefs + | None -> + Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs + +let compile_constant env sigma prefix ~interactive con cb = + match cb.const_proj with + | None -> + let u = + if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in + begin match cb.const_body with + | Def t -> + let t = Mod_subst.force_constr t in + let code = lambda_of_constr env sigma t in + if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); + let is_lazy = is_lazy prefix t in + let code = if is_lazy then mk_lazy code else code in + let name = + if interactive then LinkedInteractive prefix + else Linked prefix + in + let l = con_label con in + let auxdefs,code = + if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code + else + let univ = fresh_univ () in + let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in + (auxdefs,mkMLlam [|univ|] code) + in + if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code"); + let code = + optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs) + in + if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code"); + code, name + | _ -> + let i = push_symbol (SymbConst con) in + let args = + if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|] + else [|get_const_code i|] + in + (* + let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) + *) + [Glet(Gconstant ("",(con,u)), mkMLapp (MLprimitive Mk_const) args)], + if interactive then LinkedInteractive prefix + else Linked prefix + end + | Some pb -> + let u = Univ.Instance.empty in + let mind = pb.proj_ind in + let ind = (mind,0) in + let mib = lookup_mind mind env in + let oib = mib.mind_packets.(0) in + let tbl = oib.mind_reloc_tbl in + (* Building info *) + let prefix = get_mind_prefix env mind in + let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; + ci_cstr_nargs = [|0|]; + ci_cstr_ndecls = [||] (*FIXME*); + ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in + let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; + asw_reloc = tbl; asw_finite = true } in + let c_uid = fresh_lname Anonymous in + let _, arity = tbl.(0) in + let ci_uid = fresh_lname Anonymous in + let cargs = Array.init arity + (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) + in + let i = push_symbol (SymbConst con) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in + let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in + let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let gn = Gproj ("",con) in + let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in + let arg = fargs.(pb.proj_npars) in + Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal + arg|]))):: + [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix + +let loaded_native_files = ref ([] : string list) + +let is_loaded_native_file s = String.List.mem s !loaded_native_files + +let register_native_file s = + if not (is_loaded_native_file s) then + loaded_native_files := s :: !loaded_native_files + +let is_code_loaded ~interactive name = + match !name with + | NotLinked -> false + | LinkedInteractive s -> + if (interactive && is_loaded_native_file s) then true + else (name := NotLinked; false) + | Linked s -> + if is_loaded_native_file s then true + else (name := NotLinked; false) + +let param_name = Name (id_of_string "params") +let arg_name = Name (id_of_string "arg") + +let compile_mind prefix ~interactive mb mind stack = + let u = Declareops.inductive_instance mb in + let f i stack ob = + let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd (mind,i)) in + let name = Gind ("", ((mind, i), u)) in + let accu = + let args = + if Univ.Instance.is_empty u then + [|get_ind_code j; MLarray [||]|] + else [|get_ind_code j|] + in + Glet(name, MLapp (MLprimitive Mk_ind, args)) + in + let nparams = mb.mind_nparams in + let params = + Array.init nparams (fun i -> {lname = param_name; luid = i}) in + let add_construct j acc (_,arity) = + let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in + let c = (mind,i), (j+1) in + Glet(Gconstruct ("",(c,u)), + mkMLlam (Array.append params args) + (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc + in + Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + in + Array.fold_left_i f stack mb.mind_packets + +type code_location_update = + link_info ref * link_info +type code_location_updates = + code_location_update Mindmap_env.t * code_location_update Cmap_env.t + +type linkable_code = global list * code_location_updates + +let empty_updates = Mindmap_env.empty, Cmap_env.empty + +let compile_mind_deps env prefix ~interactive + (comp_stack, (mind_updates, const_updates) as init) mind = + let mib,nameref = lookup_mind_key mind env in + if is_code_loaded ~interactive nameref + || Mindmap_env.mem mind mind_updates + then init + else + let comp_stack = + compile_mind prefix ~interactive mib mind comp_stack + in + let name = + if interactive then LinkedInteractive prefix + else Linked prefix + in + let upd = (nameref, name) in + let mind_updates = Mindmap_env.add mind upd mind_updates in + (comp_stack, (mind_updates, const_updates)) + +(* This function compiles all necessary dependencies of t, and generates code in + reverse order, as well as linking information updates *) +let rec compile_deps env sigma prefix ~interactive init t = + match kind_of_term t with + | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind + | Const c -> + let c,u = get_allias env c in + let cb,(nameref,_) = lookup_constant_key c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive nameref + || (Cmap_env.mem c const_updates) + then init + else + let comp_stack, (mind_updates, const_updates) = match cb.const_body with + | Def t -> + compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) + | _ -> init + in + let code, name = + compile_constant env sigma prefix ~interactive c cb + in + let comp_stack = code@comp_stack in + let const_updates = Cmap_env.add c (nameref, name) const_updates in + comp_stack, (mind_updates, const_updates) + | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind + | Proj (p,c) -> + let term = mkApp (mkConst (Projection.constant p), [|c|]) in + compile_deps env sigma prefix ~interactive init term + | Case (ci, p, c, ac) -> + let mind = fst ci.ci_ind in + let init = compile_mind_deps env prefix ~interactive init mind in + fold_constr (compile_deps env sigma prefix ~interactive) init t + | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t + +let compile_constant_field env prefix con acc cb = + let (gl, _) = + compile_constant ~interactive:false env empty_evars prefix + con cb + in + gl@acc + +let compile_mind_field prefix mp l acc mb = + let mind = MutInd.make2 mp l in + compile_mind prefix ~interactive:false mb mind acc + +let mk_open s = Gopen s + +let mk_internal_let s code = + Glet(Ginternal s, code) + +(* ML Code for conversion function *) +let mk_conv_code env sigma prefix t1 t2 = + clear_symb_tbl (); + clear_global_tbl (); + let gl, (mind_updates, const_updates) = + let init = ([], empty_updates) in + compile_deps env sigma prefix ~interactive:true init t1 + in + let gl, (mind_updates, const_updates) = + let init = (gl, (mind_updates, const_updates)) in + compile_deps env sigma prefix ~interactive:true init t2 + in + let code1 = lambda_of_constr env sigma t1 in + let code2 = lambda_of_constr env sigma t2 in + let (gl,code1) = compile_with_fv env sigma None gl None code1 in + let (gl,code2) = compile_with_fv env sigma None gl None code2 in + let t1 = mk_internal_let "t1" code1 in + let t2 = mk_internal_let "t2" code2 in + let g1 = MLglobal (Ginternal "t1") in + let g2 = MLglobal (Ginternal "t2") in + let setref1 = Glet(Ginternal "_", MLsetref("rt1",g1)) in + let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in + let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in + let header = Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_symbols_tbl"), + [|MLglobal (Ginternal "()")|])) in + header::gl, (mind_updates, const_updates) + +let mk_norm_code env sigma prefix t = + clear_symb_tbl (); + clear_global_tbl (); + let gl, (mind_updates, const_updates) = + let init = ([], empty_updates) in + compile_deps env sigma prefix ~interactive:true init t + in + let code = lambda_of_constr env sigma t in + let (gl,code) = compile_with_fv env sigma None gl None code in + let t1 = mk_internal_let "t1" code in + let g1 = MLglobal (Ginternal "t1") in + let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in + let gl = List.rev (setref :: t1 :: gl) in + let header = Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_symbols_tbl"), + [|MLglobal (Ginternal "()")|])) in + header::gl, (mind_updates, const_updates) + +let mk_library_header dir = + let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in + [Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_library_symbols_tbl"), + [|MLglobal (Ginternal libname)|]))] + +let update_location (r,v) = r := v + +let update_locations (ind_updates,const_updates) = + Mindmap_env.iter (fun _ -> update_location) ind_updates; + Cmap_env.iter (fun _ -> update_location) const_updates + +let add_header_comment mlcode s = + Gcomment s :: mlcode + +(* vim: set filetype=ocaml foldmethod=marker: *) -- cgit v1.2.3