From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- engine/termops.ml | 101 +++++++++++++++++++++++++++++++++--------------------- 1 file changed, 62 insertions(+), 39 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 3dfb0c34..a343ad3c 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -22,11 +22,13 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration +module Internal = struct + (* Sorts and sort family *) let print_sort = function - | Prop Pos -> (str "Set") - | Prop Null -> (str "Prop") + | Set -> (str "Set") + | Prop -> (str "Prop") | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function @@ -47,7 +49,9 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = let pr_puniverses p u = if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" + +(* Minimalistic constr printer, typically for debugging *) let rec pr_constr c = match kind c with | Rel n -> str "#"++int n @@ -96,9 +100,16 @@ let rec pr_constr c = match kind c with cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") -let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) +let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c) +let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c) +let term_printer = ref debug_print_constr_env + let print_constr_env env sigma t = !term_printer env sigma t -let print_constr t = !term_printer (Global.env()) Evd.empty t +let print_constr t = + let env = Global.env () in + let evd = Evd.from_env env in + !term_printer env evd t + let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -111,11 +122,11 @@ let pr_evar_suggested_name evk sigma = | None -> match evi.evar_source with | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id | _,Evar_kinds.VarInstance id -> id - | _,Evar_kinds.QuestionMark (_,Name id) -> id + | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" | _ -> let env = reset_with_named_context evi.evar_hyps (Global.env()) in - Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous + Namegen.id_of_name_using_hdchar env sigma evi.evar_concl Anonymous in let names = EvMap.mapi base_id (undefined_map sigma) in let id = EvMap.find evk names in @@ -154,7 +165,7 @@ let protect f x = with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) let print_kconstr a = - protect (fun c -> print_constr (EConstr.of_constr c)) a + protect (fun c -> print_constr c) a let pr_meta_map evd = let open Evd in @@ -197,17 +208,21 @@ let pr_evar_source = function let print_constr = print_kconstr in let id = Option.get ido in str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ - spc () ++ print_constr (printable_constr_of_global c) + spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> let print_constr = print_kconstr in - pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind) + pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind) | Evar_kinds.GoalEvar -> str "goal evar" | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id - | Evar_kinds.SubEvar evk -> - str "subterm of " ++ Evar.print evk + | Evar_kinds.SubEvar (where,evk) -> + (match where with + | None -> str "subterm of " + | Some Evar_kinds.Body -> str "body of " + | Some Evar_kinds.Domain -> str "domain of " + | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk let pr_evar_info evi = let open Evd in @@ -252,7 +267,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc in Evd.fold fold sigma EvMap.empty @@ -290,7 +305,7 @@ let has_no_evar sigma = with Exit -> false let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) -let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l +let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l let pr_evar_universe_context ctx = let open UState in @@ -302,7 +317,7 @@ let pr_evar_universe_context ctx = str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) @@ -310,7 +325,8 @@ let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function | RelDecl.LocalAssum (n,_) -> Name.print n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " + ++ print_constr (EConstr.of_constr b) ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in @@ -331,11 +347,11 @@ let pr_evar_constraints sigma pbs = Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++ + protect (print_constr_env env sigma) t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2) + spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2 in prlist_with_sep fnl pr_evconstr pbs @@ -429,27 +445,29 @@ let pr_metaset metas = let pr_var_decl env decl = let open NamedDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -771,24 +789,23 @@ let map_constr_with_full_binders sigma g f l cstr = let fold_constr_with_full_binders sigma g f n acc c = let open RelDecl in - let inj c = EConstr.Unsafe.to_constr c in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -847,6 +864,13 @@ let occur_meta_or_existential sigma c = | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true +let occur_metavariable sigma m c = + let rec occrec c = match EConstr.kind sigma c with + | Meta m' -> if Int.equal m m' then raise Occur + | _ -> EConstr.iter sigma occrec c + in + try occrec c; false with Occur -> true + let occur_evar sigma n c = let rec occur_rec c = match EConstr.kind sigma c with | Evar (sp,_) when Evar.equal sp n -> raise Occur @@ -926,7 +950,7 @@ let dependent_main noevar sigma m t = match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); - CArray.Fun1.iter deprec m + Array.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) | _, Cast (c,_,_) when noevar && isMeta sigma c -> () @@ -964,9 +988,6 @@ let count_occurrences sigma m t = countrec m t; !n -(* Synonymous *) -let occur_term = dependent - let pop t = EConstr.Vars.lift (-1) t (***************************) @@ -1149,15 +1170,14 @@ let is_template_polymorphic env sigma f = let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb == Reduction.CUMUL - | (Type u1, Type u2) -> true - | _ -> false + | Prop, Prop | Set, Set | Type _, Type _ -> true + | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL + | Set, Prop | Type _, Prop | Type _, Set -> false let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Null -> true + | Prop -> true | _ -> false end | Cast (c,_,_) -> is_Prop sigma c @@ -1166,7 +1186,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with let rec is_Set sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Pos -> true + | Set -> true | _ -> false end | Cast (c,_,_) -> is_Set sigma c @@ -1369,7 +1389,7 @@ let smash_rel_context sign = let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = - try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false + try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false let map_rel_decl f = function | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t) @@ -1495,3 +1515,6 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 +end + +include Internal -- cgit v1.2.3