diff options
-rw-r--r-- | checker/checker.ml | 10 | ||||
-rw-r--r-- | checker/declarations.ml | 54 | ||||
-rw-r--r-- | checker/include | 24 | ||||
-rw-r--r-- | checker/indtypes.ml | 7 | ||||
-rw-r--r-- | checker/modops.ml | 9 | ||||
-rw-r--r-- | checker/safe_typing.ml | 3 | ||||
-rw-r--r-- | checker/validate.ml | 15 |
7 files changed, 69 insertions, 53 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 712566a00..e15c37e67 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -295,7 +295,7 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise)++report()) -let parse_args() = +let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> @@ -340,7 +340,7 @@ let parse_args() = | s :: rem -> add_compile s; parse rem in try - parse (List.tl (Array.to_list Sys.argv)) + parse (List.tl (Array.to_list argv)) with | UserError(_,s) as e -> begin try @@ -354,12 +354,12 @@ let parse_args() = (* To prevent from doing the initialization twice *) let initialized = ref false -let init() = +let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) try - parse_args(); + parse_args argv; if_verbose print_header (); init_load_path (); engage (); @@ -370,6 +370,8 @@ let init() = exit 1 end +let init() = init_with_argv Sys.argv + let run () = try compile_files (); diff --git a/checker/declarations.ml b/checker/declarations.ml index 3211cc28f..95d1f2bd1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -482,19 +482,16 @@ let subst_mps sub = type 'a lazy_subst = | LSval of 'a - | LSlazy of substitution * 'a + | LSlazy of substitution list * 'a type 'a substituted = 'a lazy_subst ref -let from_val a = ref (LSval a) +let val_substituted val_a = + val_ref + (val_sum "constr_substituted" 0 + [|[|val_a|];[|val_list val_subst;val_a|]|]) -let force fsubst r = - match !r with - | LSval a -> a - | LSlazy(s,a) -> - let a' = fsubst s a in - r := LSval a'; - a' +let from_val a = ref (LSval a) let mp_in_key mp key = let rec mp_rec mp1 = @@ -606,21 +603,27 @@ let join (subst1 : substitution) (subst2 : substitution) = let subst = Umap.mapi (apply_subst subst2) subst1 in (Umap.fold Umap.add subst2 subst) + +let force fsubst r = + match !r with + | LSval a -> a + | LSlazy(s,a) -> + let subst = List.fold_left join empty_subst (List.rev s) in + let a' = fsubst subst a in + r := LSval a'; + a' + let subst_substituted s r = match !r with - | LSval a -> ref (LSlazy(s,a)) + | LSval a -> ref (LSlazy([s],a)) | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) + ref (LSlazy(s::s',a)) let force_constr = force subst_mps type constr_substituted = constr substituted -let val_cstr_subst = - val_ref - (val_sum "constr_substituted" 0 - [|[|val_constr|];[|val_subst;val_constr|]|]) +let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted @@ -635,8 +638,13 @@ type constant_body = { const_inline : bool} let val_cb = val_tuple "constant_body" - [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs; - val_bool; val_bool |] + [|val_nctxt; + val_opt val_cstr_subst; + val_cst_type; + no_val; + val_cstrs; + val_bool; + val_bool |] let subst_rel_declaration sub (id,copt,t as x) = @@ -791,7 +799,7 @@ type mutual_inductive_body = { } let val_ind_pack = val_tuple "mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; - val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|] + val_int; val_int; val_rctxt;val_cstrs|] let subst_arity sub = function @@ -821,7 +829,7 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; @@ -896,16 +904,16 @@ and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o and val_seb o = val_sum "struct_expr_body" 0 [|[|val_mp|]; (* SEBident *) [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) - [|val_sb|]; (* SEBstruct *) [|val_seb;val_seb;val_cstrs|]; (* SEBapply *) + [|val_sb|]; (* SEBstruct *) [|val_seb;val_with|] (* SEBwith *) |] o and val_with o = val_sum "with_declaration_body" 0 [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o and val_module o = val_tuple "module_body" - [|val_mp;val_opt val_seb;val_opt val_seb; - val_seb;val_cstrs;val_res;no_val|] o + [|val_mp;val_opt val_seb;val_seb; + val_opt val_seb;val_cstrs;val_res;no_val|] o and val_modtype o = val_tuple "module_type_body" [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o diff --git a/checker/include b/checker/include index 331eb45c1..b7d46d4b3 100644 --- a/checker/include +++ b/checker/include @@ -8,20 +8,26 @@ (mainly run_l and norec). *) -#cd ".." +#cd "..";; #directory "lib";; #directory "kernel";; #directory "checker";; +#directory "+camlp4";; +#directory "+camlp5";; #load "unix.cma";; #load "str.cma";; #load "gramlib.cma";; +(*#load "toplevellib.cma";; + +#directory "/usr/lib/ocaml/compiler-libs/utils";; +let _ = Clflags.recursive_types:=true;; +*) #load "check.cma";; open Typeops;; open Check;; - open Pp;; open Util;; open Names;; @@ -70,10 +76,11 @@ let prenv e = pp pe;; *) +(* let prsub s = let string_of_mp mp = let s = string_of_mp mp in - (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in + (match mp with MPbound _ -> "#bound."|_->"")^s in pp (hv 0 (fold_subst (fun msid mp strm -> @@ -86,6 +93,7 @@ let prsub s = str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++ str (string_of_mp mp) ++ fnl() ++ strm) s (mt()))) ;; +*) #install_printer prid;; #install_printer prcon;; @@ -100,10 +108,10 @@ let prsub s = #install_printer prcstrs;; (*#install_printer prus;;*) (*#install_printer prenv;;*) -(*#install_printer prenvu;;*) -#install_printer prsub;; +(*#install_printer prenvu;; +#install_printer prsub;;*) -Checker.init();; +Checker.init_with_argv [|""|];; Flags.make_silent false;; Flags.debug := true;; Sys.catch_break true;; @@ -114,7 +122,7 @@ let module_of_file f = ;; let mod_access m fld = match m.mod_expr with - Some(SEBstruct(msid,l)) -> List.assoc fld l + Some(SEBstruct l) -> List.assoc fld l | _ -> failwith "bad structure type" ;; @@ -153,7 +161,7 @@ let read_mod s f = engagement option);; let deref_mod md s = - let (Some (SEBstruct(msid,l))) = md.mod_expr in + let (Some (SEBstruct l)) = md.mod_expr in List.assoc (label_of_id(id_of_string s)) l ;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index e0aa9e7c3..de57c50a7 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -22,7 +22,7 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl @@ -36,8 +36,9 @@ let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) let prcon c = - let (mp,_,l) = repr_con c in - str(string_of_mp mp ^ "." ^ string_of_label l) + let ck = canonical_con c in + let uk = user_con c in + if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. Could be refined more... *) diff --git a/checker/modops.ml b/checker/modops.ml index 3d07135d1..de0d6c7e9 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -127,10 +127,7 @@ let strengthen_const env mp_from l cb resolver = let rec strengthen_mod env mp_from mp_to mb = - assert(mp_from = mb.mod_mp); -(* if mp_in_delta mb.mod_mp mb.mod_delta then - mb - else*) + assert(mp_from = mb.mod_mp); match mb.mod_type with | SEBstruct (sign) -> let resolve_out,sign_out = @@ -180,10 +177,6 @@ and strengthen_sig env mp_from sign mp_to resolver = resolve_out,item::rest' let strengthen env mtb mp = -(* if mp_in_delta mtb.typ_mp mtb.typ_delta then - (* in this case mtb has already been strengthened*) - mtb - else*) match mtb.typ_expr with | SEBstruct (sign) -> let resolve_out,sign_out = diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index da0e63c23..8f5d45732 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -131,7 +131,8 @@ let import file (dp,mb,depends,engmt as vo) digest = full_add_module dp mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt) digest = +let unsafe_import file (dp,mb,depends,engmt as vo) digest = +(* if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*) let env = !genv in check_imports (errorlabstrm"unsafe_import") dp env depends; check_engagement env engmt; diff --git a/checker/validate.ml b/checker/validate.ml index 804bf7dfe..704468169 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -41,6 +41,8 @@ let pr_obj o = pr_obj_rec o; Format.print_newline() exception ValidObjError of string * Obj.t let fail o s = raise (ValidObjError(s,o)) +let ep s1 f s2 = f (s1^"/"^s2) + let apply debug f x = let o = Obj.repr x in try f o @@ -49,7 +51,7 @@ let apply debug f x = print_endline ("Validation failed: "^msg); pr_obj obj end; - failwith "validation failed" + failwith "vo structure validation failed" (* data not validated *) let no_val (o:Obj.t) = () @@ -71,8 +73,7 @@ let val_block s o = let val_tuple s v o = let n = Array.length v in val_block ("tuple: "^s) o; - if Obj.size o = n then - Array.iteri (fun i f -> f (Obj.field o i)) v + if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v else fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)) @@ -88,7 +89,7 @@ let val_sum s cc vv o = let n = Array.length vv in let i = Obj.tag o in if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o - else fail o ("bad tag in (sum type) "^s^": max is "^string_of_int i)) + else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i)) else if Obj.is_int o then let (n:int) = Obj.magic o in (if n<0 || n>=cc then @@ -161,9 +162,11 @@ let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|] let val_mp = val_rec_sum "module_path" 0 - (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|]) + (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) -let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] +let val_kn = + let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] in + val_tuple "kn*kn" [|val_kn;val_kn|] let val_ind = val_tuple "inductive"[|val_kn;val_int|] let val_cstr = val_tuple "constructor"[|val_ind;val_int|] |