summaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml8
-rw-r--r--checker/checker.ml10
-rw-r--r--checker/indtypes.ml15
-rw-r--r--checker/mod_checking.ml132
-rw-r--r--checker/reduction.ml14
-rw-r--r--checker/safe_typing.ml4
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*)