diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 8 | ||||
| -rw-r--r-- | checker/checker.ml | 10 | ||||
| -rw-r--r-- | checker/indtypes.ml | 15 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 132 | ||||
| -rw-r--r-- | checker/reduction.ml | 14 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 4 |
6 files changed, 110 insertions, 73 deletions
diff --git a/checker/check.ml b/checker/check.ml index e91516c7..40ac604e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -23,8 +23,7 @@ type section_path = { dirpath : string list ; basename : string } let dir_of_path p = - make_dirpath - (id_of_string p.basename :: List.map id_of_string p.dirpath) + make_dirpath (List.map id_of_string p.dirpath) let path_of_dirpath dir = match repr_dirpath dir with [] -> failwith "path_of_dirpath" @@ -166,6 +165,9 @@ let remove_load_path dir = load_paths := list_filter2 (fun p d -> p <> dir) !load_paths let add_load_path (phys_path,coq_path) = + if !Flags.debug then + msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + str phys_path); let phys_path = canonical_path_name phys_path in match list_filter2 (fun p d -> p = phys_path) !load_paths with | _,[dir] -> @@ -224,7 +226,7 @@ let locate_qualified_library qid = (* Search library in loadpath *) if qid.dirpath=[] then get_load_paths () else - (* we assume dir is an absolute dirpath *) + (* we assume qid is an absolute dirpath *) load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; diff --git a/checker/checker.ml b/checker/checker.ml index 7de25835..1ed094cf 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -191,6 +191,11 @@ let print_usage_channel co command = -where print Coq's standard library location and exit -v print Coq version and exit + -boot boot mode + -o print the list of assumptions + -m print the maximum heap size + + -impredicative-set set sort Set impredicative -h, --help print this list of options " @@ -323,10 +328,9 @@ let parse_args() = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - + | "-boot" :: rem -> boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem - - | ("-o" | "-output-context") :: rem -> + | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8c84fb0f..4c9b3d61 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -19,6 +19,21 @@ open Pp open Declarations open Environ +let rec debug_string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> "bound("^string_of_mbid uid^")" + | MPself uid -> "self("^string_of_msid uid^")" + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let rec string_of_mp = function + | MPfile sl -> string_of_dirpath sl + | MPbound uid -> string_of_mbid uid + | MPself uid -> string_of_msid uid + | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + +let string_of_mp mp = + if !Flags.debug then debug_string_of_mp mp else string_of_mp mp + let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ecf8d633..379273af 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,7 +26,7 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); - let env = add_constraints cb.const_constraints env in +(* let env = add_constraints cb.const_constraints env in*) let env' = check_named_ctxt env cb.const_hyps in (match cb.const_type with NonPolymorphicType ty -> @@ -47,58 +47,6 @@ let check_constant_declaration env kn cb = (* Checking modules *) -let rec add_struct_expr_constraints env = function - | SEBident _ -> env - - | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb - - | SEBstruct (_,structure_body) -> - List.fold_left - (fun env (l,item) -> add_struct_elem_constraints env item) - env - structure_body - - | SEBapply (meb1,meb2,cst) -> -(* let g = Univ.merge_constraints cst Univ.initial_universes in -msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ - Univ.pr_universes g++str"============="++fnl()); -*) - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) - meb2) - | SEBwith(meb,With_definition_body(_,cb))-> - Environ.add_constraints cb.const_constraints - (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,cst))-> - Environ.add_constraints cst - (add_struct_expr_constraints env meb) - -and add_struct_elem_constraints env = function - | SFBconst cb -> Environ.add_constraints cb.const_constraints env - | SFBmind mib -> Environ.add_constraints mib.mind_constraints env - | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,None) -> env - | SFBmodtype mtb -> add_modtype_constraints env mtb - -and add_module_constraints env mb = - let env = match mb.mod_expr with - | None -> env - | Some meb -> add_struct_expr_constraints env meb - in - let env = match mb.mod_type with - | None -> env - | Some mtb -> - add_struct_expr_constraints env mtb - in - Environ.add_constraints mb.mod_constraints env - -and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb.typ_expr - exception Not_path let path_of_mexpr = function @@ -307,19 +255,18 @@ and check_module_type env mty = check_alias mty.typ_alias sub and check_module env mb = - let env' = add_module_constraints env mb in let sub = match mb.mod_expr, mb.mod_type with | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" - | None, Some mtb -> check_modexpr env' mtb + | None, Some mtb -> check_modexpr env mtb | Some mexpr, _ -> - let sub1 = check_modexpr env' mexpr in + let sub1 = check_modexpr env mexpr in (match mb.mod_type with | None -> sub1 | Some mte -> - let sub2 = check_modexpr env' mte in + let sub2 = check_modexpr env mte in check_subtypes env {typ_expr = mexpr; typ_strength = None; @@ -342,21 +289,22 @@ and check_structure_field (s,env) mp lab = function let mp1 = MPdot(mp,lab) in let is_fun, sub = Modops.update_subst env msb mp1 in ((if is_fun then s else join s sub), - Modops.add_module (MPdot(mp,lab)) msb - (add_module_constraints env msb)) + Modops.add_module (MPdot(mp,lab)) msb env) | SFBalias(mp2,cst) -> + (* cf Safe_typing.add_alias *) (try + let mp' = MPdot(mp,lab) in let mp2' = scrape_alias mp2 env in - let msb = lookup_module mp2' env in - (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias), - Option.fold_right add_constraints cst - (register_alias (MPdot(mp,lab)) mp2 env)) + let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in + let sub = update_subst sub (map_mp mp' mp2') in + let sub = join_alias sub (map_mp mp' mp2') in + let sub = add_mp mp' mp2' sub in + (join s sub, register_alias mp' mp2 env) with Not_found -> failwith "unkown aliased module") | SFBmodtype mty -> let kn = MPdot(mp, lab) in check_module_type env mty; - (join s mty.typ_alias, - add_modtype kn mty (add_modtype_constraints env mty)) + (join s mty.typ_alias, add_modtype kn mty env) and check_modexpr env mse = match mse with | SEBident mp -> @@ -396,3 +344,57 @@ and check_modexpr env mse = match mse with List.fold_left (fun env (lab,mb) -> check_structure_field env mp lab mb) (empty_subst,env) msb in sub + +(* +let rec add_struct_expr_constraints env = function + | SEBident _ -> env + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb + + | SEBstruct (_,structure_body) -> + List.fold_left + (fun env (l,item) -> add_struct_elem_constraints env item) + env + structure_body + + | SEBapply (meb1,meb2,cst) -> +(* let g = Univ.merge_constraints cst Univ.initial_universes in +msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ + Univ.pr_universes g++str"============="++fnl()); +*) + Environ.add_constraints cst + (add_struct_expr_constraints + (add_struct_expr_constraints env meb1) + meb2) + | SEBwith(meb,With_definition_body(_,cb))-> + Environ.add_constraints cb.const_constraints + (add_struct_expr_constraints env meb) + | SEBwith(meb,With_module_body(_,_,cst))-> + Environ.add_constraints cst + (add_struct_expr_constraints env meb) + +and add_struct_elem_constraints env = function + | SFBconst cb -> Environ.add_constraints cb.const_constraints env + | SFBmind mib -> Environ.add_constraints mib.mind_constraints env + | SFBmodule mb -> add_module_constraints env mb + | SFBalias (mp,Some cst) -> Environ.add_constraints cst env + | SFBalias (mp,None) -> env + | SFBmodtype mtb -> add_modtype_constraints env mtb + +and add_module_constraints env mb = + let env = match mb.mod_expr with + | None -> env + | Some meb -> add_struct_expr_constraints env meb + in + let env = match mb.mod_type with + | None -> env + | Some mtb -> + add_struct_expr_constraints env mtb + in + Environ.add_constraints mb.mod_constraints env + +and add_modtype_constraints env mtb = + add_struct_expr_constraints env mtb.typ_expr +*) diff --git a/checker/reduction.ml b/checker/reduction.ml index 49f05daf..c398f0a4 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -195,6 +195,12 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true | FLOCKED -> assert false +let oracle_order fl1 fl2 = + match fl1,fl2 with + ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false + | _, ConstKey _ -> true + | _ -> false + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = with NotConvertible -> (* else the oracle tells which constant is to be expanded *) let (app1,app2) = + if oracle_order fl1 fl2 then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> raise NotConvertible) + else match unfold_reference infos fl2 with | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) | None -> diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 4b156e7e..d5779923 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -31,7 +31,7 @@ let set_engagement c = let full_add_module dp mb digest = let env = !genv in let mp = MPfile dp in - let env = add_module_constraints env mb in + let env = add_constraints mb.mod_constraints env in let env = Modops.add_module mp mb env in genv := add_digest env dp digest @@ -121,7 +121,7 @@ let import file (dp,mb,depends,engmt as vo) digest = let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module env mb; + check_module (add_constraints mb.mod_constraints env) mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) |