diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 219 |
1 files changed, 70 insertions, 149 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index ee0c3d210e..ada6311067 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -24,92 +24,16 @@ module CompactedDecl = Context.Compacted.Declaration module Internal = struct -(* Sorts and sort family *) - -let print_sort = function - | Set -> (str "Set") - | Prop -> (str "Prop") - | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") - -let pr_sort_family = function - | InSet -> (str "Set") - | InProp -> (str "Prop") - | InType -> (str "Type") - -let pr_con sp = str(Constant.to_string sp) - -let pr_fix pr_constr ((t,i),(lna,tl,bl)) = - let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in - hov 1 - (str"fix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -let pr_puniverses p u = - if Univ.Instance.is_empty u then p - 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 - | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> Id.print id - | Sort s -> print_sort s - | Cast (c,_, t) -> hov 1 - (str"(" ++ pr_constr c ++ cut() ++ - str":" ++ pr_constr t ++ str")") - | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++ - spc() ++ pr_constr c) - | Prod (Anonymous,t,c) -> hov 0 - (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ - pr_constr c ++ str")") - | Lambda (na,t,c) -> hov 1 - (str"fun " ++ Name.print na ++ str":" ++ - pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) - | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ - str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ - pr_constr c) - | App (c,l) -> hov 1 - (str"(" ++ pr_constr c ++ spc() ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") - | Evar (e,l) -> hov 1 - (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")" - | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")" - | Construct (((sp,i),j),u) -> - str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" - | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")" - | Case (ci,p,c,bl) -> v 0 - (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ - pr_constr c ++ str"of") ++ cut() ++ - prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++ - cut() ++ str"end") - | Fix f -> pr_fix pr_constr f - | CoFix(i,(lna,tl,bl)) -> - let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in - hov 1 - (str"cofix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - Name.print na ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -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 pr_sort_family = Sorts.pr_sort_family +[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] +let pr_fix = Constr.debug_print_fix +[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] -let print_constr_env env sigma t = !term_printer env sigma t -let print_constr t = - let env = Global.env () in - let evd = Evd.from_env env in - !term_printer env evd t +let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c) +let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c) +let term_printer = ref debug_print_constr_env +let print_constr_env env sigma t = !term_printer (env:env) sigma (t:Evd.econstr) let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -164,10 +88,10 @@ let protect f x = try f x with e -> str "EXCEPTION: " ++ str (Printexc.to_string e) -let print_kconstr a = - protect (fun c -> print_constr c) a +let print_kconstr env sigma a = + protect (fun c -> print_constr_env env sigma c) a -let pr_meta_map evd = +let pr_meta_map env sigma = let open Evd in let print_constr = print_kconstr in let pr_name = function @@ -177,25 +101,25 @@ let pr_meta_map evd = | (mv,Cltyp (na,b)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " : " ++ - print_constr b.rebus ++ fnl ()) + print_constr env sigma b.rebus ++ fnl ()) | (mv,Clval(na,(b,s),t)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " := " ++ - print_constr b.rebus ++ - str " : " ++ print_constr t.rebus ++ + print_constr env sigma b.rebus ++ + str " : " ++ print_constr env sigma t.rebus ++ spc () ++ pr_instance_status s ++ fnl ()) in - prlist pr_meta_binding (meta_list evd) + prlist pr_meta_binding (meta_list sigma) -let pr_decl (decl,ok) = +let pr_decl env sigma (decl,ok) = let open NamedDecl in let print_constr = print_kconstr in match decl with | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") + print_constr env sigma c ++ str (if ok then ")" else "}") -let pr_evar_source = function +let pr_evar_source env sigma = function | Evar_kinds.NamedHole id -> Id.print id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" @@ -208,11 +132,11 @@ 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 (EConstr.of_constr @@ printable_constr_of_global c) + spc () ++ print_constr env sigma (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 (EConstr.mkInd ind) + pr_nth n ++ str " argument of type " ++ print_constr env sigma (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" @@ -224,7 +148,7 @@ let pr_evar_source = function | Some Evar_kinds.Domain -> str "domain of " | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk -let pr_evar_info evi = +let pr_evar_info env sigma evi = let open Evd in let print_constr = print_kconstr in let phyps = @@ -233,23 +157,23 @@ let pr_evar_info evi = | None -> List.map (fun c -> (c, true)) (evar_context evi) | Some filter -> List.combine (evar_context evi) filter in - prlist_with_sep spc pr_decl (List.rev decls) + prlist_with_sep spc (pr_decl env sigma) (List.rev decls) with Invalid_argument _ -> str "Ill-formed filtered context" in - let pty = print_constr evi.evar_concl in + let pty = print_constr env sigma evi.evar_concl in let pb = match evi.evar_body with | Evar_empty -> mt () - | Evar_defined c -> spc() ++ str"=> " ++ print_constr c + | Evar_defined c -> spc() ++ str"=> " ++ print_constr env sigma c in let candidates = match evi.evar_body, evi.evar_candidates with | Evar_empty, Some l -> spc () ++ str "{" ++ - prlist_with_sep (fun () -> str "|") print_constr l ++ str "}" + prlist_with_sep (fun () -> str "|") (print_constr env sigma) l ++ str "}" | _ -> mt () in - let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in + let src = str "(" ++ pr_evar_source env sigma (snd evi.evar_source) ++ str ")" in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++ candidates ++ spc() ++ src) @@ -304,8 +228,8 @@ let has_no_evar sigma = try let () = Evd.fold (fun _ _ () -> raise Exit) sigma () in true with Exit -> false -let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) -let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l +let pr_evd_level sigma = UState.pr_uctx_level (Evd.evar_universe_context sigma) +let reference_of_level sigma l = UState.qualid_of_level (Evd.evar_universe_context sigma) l let pr_evar_universe_context ctx = let open UState in @@ -321,12 +245,12 @@ let pr_evar_universe_context ctx = str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) -let print_env_short env = +let print_env_short env sigma = 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 (EConstr.of_constr b) ++ str ")" + ++ print_constr env sigma (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 @@ -346,7 +270,7 @@ let pr_evar_constraints sigma pbs = naming/renaming. *) Namegen.make_all_name_different env sigma in - print_env_short env ++ spc () ++ str "|-" ++ spc () ++ + print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++ protect (print_constr_env env sigma) t1 ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" @@ -355,7 +279,7 @@ let pr_evar_constraints sigma pbs = in prlist_with_sep fnl pr_evconstr pbs -let pr_evar_map_gen with_univs pr_evars sigma = +let pr_evar_map_gen with_univs pr_evars env sigma = let uvs = Evd.evar_universe_context sigma in let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl () @@ -365,18 +289,30 @@ let pr_evar_map_gen with_univs pr_evars sigma = else str "CONSTRAINTS:" ++ brk (0, 1) ++ pr_evar_constraints sigma conv_pbs ++ fnl () + and typeclasses = + let evars = Evd.get_typeclass_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "TYPECLASSES:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () + and obligations = + let evars = Evd.get_obligation_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "OBLIGATIONS:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else - str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma + str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma in - evs ++ svs ++ cstrs ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas -let pr_evar_list sigma l = +let pr_evar_list env sigma l = let open Evd in let pr (ev, evi) = h 0 (Evar.print ev ++ - str "==" ++ pr_evar_info evi ++ + str "==" ++ pr_evar_info env sigma evi ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) @@ -399,18 +335,18 @@ let to_list d = Evd.fold fold_undef d (); !l -let pr_evar_by_depth depth sigma = match depth with +let pr_evar_by_depth depth env sigma = match depth with | None -> (* Print all evars *) - str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl() + str"EVARS:" ++ brk(0,1) ++ pr_evar_list env sigma (to_list sigma) ++ fnl() | Some n -> (* Print closure of undefined evars *) str"UNDEFINED EVARS:"++ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ brk(0,1)++ - pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl() + pr_evar_list env sigma (evar_dependency_closure n sigma) ++ fnl() -let pr_evar_by_filter filter sigma = +let pr_evar_by_filter filter env sigma = let open Evd in let elts = Evd.fold (fun evk evi accu -> (evk, evi) :: accu) sigma [] in let elts = List.rev elts in @@ -425,49 +361,49 @@ let pr_evar_by_filter filter sigma = let prdef = if List.is_empty defined then mt () else str "DEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma defined + pr_evar_list env sigma defined in let prundef = if List.is_empty undefined then mt () else str "UNDEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma undefined + pr_evar_list env sigma undefined in prdef ++ prundef -let pr_evar_map ?(with_univs=true) depth sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma +let pr_evar_map ?(with_univs=true) depth env sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth env sigma) env sigma -let pr_evar_map_filter ?(with_univs=true) filter sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma +let pr_evar_map_filter ?(with_univs=true) filter env sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter env sigma) env sigma let pr_metaset metas = str "[" ++ pr_sequence pr_meta (Evd.Metaset.elements metas) ++ str "]" let pr_var_decl env decl = let open NamedDecl in - let evd = Evd.from_env env in + let sigma = 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 c in + let pb = print_constr_env env sigma c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in + let pt = print_constr_env env sigma (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 sigma = 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 c in + let pb = print_constr_env env sigma c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in + let ptyp = print_constr_env env sigma (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) @@ -816,26 +752,11 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open RelDecl 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, 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, 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, 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 + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let g d l = g (of_rel_decl d) l in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c @@ -1187,7 +1108,7 @@ let isGlobalRef sigma c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env sigma f = +let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false |