diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | kernel/environ.ml | 19 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 25 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | kernel/sign.ml | 12 | ||||
| -rw-r--r-- | kernel/sign.mli | 3 | ||||
| -rw-r--r-- | proofs/clenv.ml | 141 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 4 |
8 files changed, 94 insertions, 120 deletions
@@ -262,7 +262,7 @@ coqbinaries:: ${COQBINARIES} world: coqbinaries states theories contrib tools $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) - $(COQMKTOP) -opt $(MLINCLUDES) -o $@ + $(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) @@ -321,7 +321,7 @@ toplevel: $(TOPLEVEL) # special binaries for debugging bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) - $(COQMKTOP) -top $(MLINCLUDES) $(CAMLDEBUG) -o $@ $(INTERFACE) + $(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) bin/parser$(EXE): contrib/interface/ctast.cmo contrib/interface/parse.cmo contrib/interface/line_parser.cmo $(PARSERREQUIRES) contrib/interface/xlate.cmo contrib/interface/vtp.cmo $(OCAMLC) -cclib -lunix -custom $(MLINCLUDES) -o $@ $(CMA) \ @@ -622,7 +622,7 @@ MINICOQCMO=$(CONFIG) $(LIBREP) $(KERNEL) \ MINICOQ=bin/minicoq$(EXE) $(MINICOQ): $(MINICOQCMO) - $(OCAMLC) $(CAMLDEBUG) $(MLINCLUDES) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) + $(OCAMLC) $(BYTEFLAGS) -o $@ -custom $(CMA) $(MINICOQCMO) $(OSDEPLIBS) archclean:: rm -f $(MINICOQ) diff --git a/kernel/environ.ml b/kernel/environ.ml index 7113b4040e..e4fc5c0e9d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -61,11 +61,10 @@ let evaluable_rel n env = with Not_found -> false -let rel_context_app f env = +let push_rel d env = { env with - env_rel_context = f env.env_rel_context } + env_rel_context = add_rel_decl d env.env_rel_context } -let push_rel d = rel_context_app (add_rel_decl d) let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = let ctxt = @@ -96,11 +95,9 @@ let evaluable_named id env = with Not_found -> false -let named_context_app f env = +let push_named d env = { env with - env_named_context = f env.env_named_context } - -let push_named d = named_context_app (Sign.add_named_decl d) + env_named_context = Sign.add_named_decl d env.env_named_context } let reset_context env = { env with @@ -125,10 +122,6 @@ let lookup_constant sp env = Spmap.find sp env.env_globals.env_constants let add_constant sp cb env = - let _ = - try - let _ = lookup_constant sp env in failwith "already declared constant" - with Not_found -> () in let new_constants = Spmap.add sp cb env.env_globals.env_constants in let new_locals = (Constant,sp)::env.env_globals.env_locals in let new_globals = @@ -167,10 +160,6 @@ let lookup_mind sp env = Spmap.find sp env.env_globals.env_inductives let add_mind sp mib env = - let _ = - try - let _ = lookup_mind sp env in failwith "already defined inductive" - with Not_found -> () in let new_inds = Spmap.add sp mib env.env_globals.env_inductives in let new_locals = (Inductive,sp)::env.env_globals.env_locals in let new_globals = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ad36e2941b..f424f79dbf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -54,7 +54,20 @@ let push_rel_or_named_def push (id,b,topt) env = let env'' = push (id,Some j.uj_val,typ) env' in (cst,env'') -let push_named_def = push_rel_or_named_def push_named + +(* Same as push_named, but check that the variable is not already + there. Should *not* be done in Environ because tactics add temporary + hypothesis many many times, and the check performed here would + cost too much. *) +let safe_push_named (id,_,_ as d) env = + let _ = + try + let _ = lookup_named id env in + error ("identifier "^string_of_id id^" already defined") + with Not_found -> () in + push_named d env + +let push_named_def = push_rel_or_named_def safe_push_named let push_rel_def = push_rel_or_named_def push_rel let push_rel_or_named_assum push (id,t) env = @@ -112,11 +125,21 @@ let add_global_declaration sp env (body,typ,cst,op) = (*s Global and local constant declaration. *) let add_constant sp ce env = + let _ = + try + let _ = lookup_constant sp env in + error ("constant "^string_of_path sp^" already declared") + with Not_found -> () in add_global_declaration sp env (safe_infer_declaration env ce) (* Insertion of inductive types. *) let add_mind sp mie env = + let _ = + try + let _ = lookup_mind sp env in + error ("inductive "^string_of_path sp^" already declared") + with Not_found -> () in let mib = check_inductive env mie in let cst = mib.mind_constraints in Environ.add_mind sp mib (add_constraints cst env) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 071a67224a..10357f407c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -45,11 +45,11 @@ type global_declaration = | GlobalRecipe of Cooking.recipe val add_constant : - section_path -> global_declaration -> safe_environment -> safe_environment + constant -> global_declaration -> safe_environment -> safe_environment (* Adding an inductive type *) val add_mind : - section_path -> Indtypes.mutual_inductive_entry -> safe_environment -> + mutual_inductive -> Indtypes.mutual_inductive_entry -> safe_environment -> safe_environment (* Adding universe constraints *) diff --git a/kernel/sign.ml b/kernel/sign.ml index da6ec5a11d..f0c275fa37 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -19,19 +19,13 @@ type named_context = named_declaration list let empty_named_context = [] +let add_named_decl d sign = d::sign let rec lookup_named id = function | (id',_,_ as decl) :: _ when id=id' -> decl | _ :: sign -> lookup_named id sign | [] -> raise Not_found - -let add_named_decl (id,_,_ as d) sign = - try - let _ = lookup_named id sign in - failwith ("identifier "^string_of_id id^" already defined") - with _ -> d::sign - let named_context_length = List.length let instance_from_named_context sign = @@ -99,10 +93,6 @@ let push_named_to_rel_context hyps ctxt = (* Term constructors *) (*********************************) -let it_mkNamedProd_or_LetIn = - List.fold_left (fun c d -> mkNamedProd_or_LetIn d c) -let it_mkNamedLambda_or_LetIn = - List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) diff --git a/kernel/sign.mli b/kernel/sign.mli index 6ba3e4fff7..e5de5613d8 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -58,9 +58,6 @@ val fold_rel_context_reverse : (*s Term constructors *) -val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr -val it_mkNamedProd_or_LetIn : types -> named_context -> types - val it_mkLambda_or_LetIn : constr -> rel_context -> constr val it_mkProd_or_LetIn : types -> rel_context -> types diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 6fbe69647e..0c76be8df1 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -124,93 +124,69 @@ let mimick_evar hdc nargs sp wc = Attention : pas d'unification entre les différences instances d'une même meta ou evar, il peut rester des doublons *) +(* Unification order: *) +(* Left to right: unifies first argument and then the other arguments *) +let unify_l2r x = List.rev x +(* Right to left: unifies last argument and then the other arguments *) +let unify_r2l x = x + +let sort_eqns = unify_r2l + + + let unify_0 cv_pb wc m n = let env = w_env wc and sigma = w_Underlying wc in + let trivial_unify pb substn m n = + if (not(occur_meta m)) & is_fconv pb env sigma m n then substn + else error_cannot_unify (m,n) in let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n = let cM = Evarutil.whd_castappevar sigma m and cN = Evarutil.whd_castappevar sigma n in - try - match (kind_of_term cM,kind_of_term cN) with - | Cast (c,_), _ -> unirec_rec pb substn c cN - | _, Cast (c,_) -> unirec_rec pb substn cM c - | Meta k1, Meta k2 -> - if k1 < k2 then (k1,cN)::metasubst,evarsubst - else if k1 = k2 then substn - else (k2,cM)::metasubst,evarsubst - | Meta k, _ -> (k,cN)::metasubst,evarsubst - | _, Meta k -> (k,cM)::metasubst,evarsubst - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> - unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 - - | App (f1,l1), App (f2,l2) -> - let len1 = Array.length l1 - and len2 = Array.length l2 in - if len1 = len2 then - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn f1 f2) l1 l2 + match (kind_of_term cM,kind_of_term cN) with + | Meta k1, Meta k2 -> + if k1 < k2 then (k1,cN)::metasubst,evarsubst + else if k1 = k2 then substn + else (k2,cM)::metasubst,evarsubst + | Meta k, _ -> (k,cN)::metasubst,evarsubst + | _, Meta k -> (k,cM)::metasubst,evarsubst + | Evar _, _ -> metasubst,((cM,cN)::evarsubst) + | _, Evar _ -> metasubst,((cN,cM)::evarsubst) + + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 + | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN + | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) + + | App (f1,l1), App (f2,l2) -> + let len1 = Array.length l1 + and len2 = Array.length l2 in + let (f1,l1,f2,l2) = + if len1 = len2 then (f1,l1,f2,l2) else if len1 < len2 then let extras,restl2 = array_chop (len2-len1) l2 in - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn f1 (appvect (f2,extras))) - l1 restl2 + (f1, l1, appvect (f2,extras), restl2) else let extras,restl1 = array_chop (len1-len2) l1 in - array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV substn (appvect (f1,extras)) f2) - restl1 l2 - - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> + (appvect (f1,extras), restl1, f2, l2) in + (try array_fold_left2 (unirec_rec CONV) - (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 - - | Construct _, Construct _ -> - if is_conv env sigma cM cN then - substn - else - error_cannot_unify (m,n) - - | Ind _, Ind _ -> - if is_conv env sigma cM cN then - substn - else - error_cannot_unify (m,n) - - | Evar _, _ -> - metasubst,((cM,cN)::evarsubst) - | _, Evar _ -> - metasubst,((cN,cM)::evarsubst) - - | (Const _ | Var _ | Rel _), _ -> - if is_conv env sigma cM cN then - substn - else - error_cannot_unify (m,n) - - | _, (Const _ | Var _| Rel _) -> - if (not (occur_meta cM)) & is_conv env sigma cM cN then - substn - else - error_cannot_unify (m,n) - - | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN - | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) - - | _ -> error_cannot_unify (m,n) - - with ex when catchable_exception ex -> - if (not(occur_meta cM)) & is_fconv pb env sigma cM cN then - substn - else - raise ex - - in - if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then - ([],[]) - else - unirec_rec cv_pb ([],[]) m n + (unirec_rec CONV substn f1 f2) l1 l2 + with ex when catchable_exception ex -> + trivial_unify pb substn cM cN) + | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> + array_fold_left2 (unirec_rec CONV) + (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 + + | _ -> trivial_unify pb substn cM cN + + in + if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then + ([],[]) + else + unirec_rec cv_pb ([],[]) m n (* Unification @@ -264,7 +240,7 @@ let unify_0 cv_pb wc m n = let rec w_Unify cv_pb m n wc = let (mc',ec') = unify_0 cv_pb wc m n in - w_resrec (List.rev mc') (List.rev ec') wc + w_resrec mc' ec' wc and w_resrec metas evars wc = match evars with @@ -609,7 +585,7 @@ let clenv_merge with_types = | Evar (evn,_) -> if w_defined_evar clenv.hook evn then let (metas',evars') = unify_0 CONV clenv.hook rhs lhs in - clenv_resrec (List.rev metas'@metas) (List.rev evars'@t) clenv + clenv_resrec (metas'@metas) (evars'@t) clenv else begin let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs @@ -634,7 +610,7 @@ let clenv_merge with_types = if clenv_defined clenv mv then let (metas',evars') = unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in - clenv_resrec (List.rev metas'@t) (List.rev evars') clenv + clenv_resrec (metas'@t) evars' clenv else let mc,ec = let mvty = clenv_instance_type clenv mv in @@ -645,8 +621,7 @@ let clenv_merge with_types = unify_0 CUMUL clenv.hook nty mvty with e when Logic.catchable_exception e -> ([],[])) else ([],[]) in - clenv_resrec (List.rev mc@t) (List.rev ec) - (clenv_assign mv n clenv) + clenv_resrec (mc@t) ec (clenv_assign mv n clenv) in clenv_resrec @@ -662,7 +637,7 @@ let clenv_merge with_types = let clenv_unify_core_0 with_types cv_pb m n clenv = let (mc,ec) = unify_0 cv_pb clenv.hook m n in - clenv_merge with_types (List.rev mc) (List.rev ec) clenv + clenv_merge with_types mc ec clenv let clenv_unify_0 = clenv_unify_core_0 false let clenv_typed_unify = clenv_unify_core_0 true @@ -827,7 +802,7 @@ let clenv_unify allow_K cv_pb ty1 ty2 clenv = with ex when catchable_exception ex -> error "Cannot solve a second-order unification problem") - | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv + | _ -> clenv_typed_unify cv_pb ty1 ty2 clenv (* [clenv_bchain mv clenv' clenv] diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 32b5a47b45..7f20f90c7b 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -103,11 +103,11 @@ let rec explain_exn_default = function hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") | Assert_failure (s,b,e) -> hov 0 (str "Anomaly: assert failure" ++ spc () ++ - if s <> "" then + (if s <> "" then (str ("(file \"" ^ s ^ "\", characters ") ++ int b ++ str "-" ++ int e ++ str ")") else - (mt ()) ++ + (mt ())) ++ report ()) | reraise -> hov 0 (str "Anomaly: Uncaught exception " ++ |