diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 47 |
1 files changed, 24 insertions, 23 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 76f707f94..a71bdff31 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -12,6 +12,7 @@ open Util open Names open Nameops open Term +open Constr open Vars open Environ @@ -31,7 +32,7 @@ let pr_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") -let pr_con sp = str(string_of_con sp) +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 @@ -46,16 +47,16 @@ 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"*)" -let rec pr_constr c = match kind_of_term c with +let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> pr_id id + | 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 " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++ + (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() ++ @@ -74,9 +75,9 @@ let rec pr_constr c = match kind_of_term c with (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 (pr_mind sp ++ str"," ++ int i) 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 (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" + 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 " ++ @@ -129,9 +130,9 @@ let pr_existential_key sigma evk = let open Evd in match evar_ident evk sigma with | None -> - str "?" ++ pr_id (pr_evar_suggested_name evk sigma) + str "?" ++ Id.print (pr_evar_suggested_name evk sigma) | Some id -> - str "?" ++ pr_id id + str "?" ++ Id.print id let pr_instance_status (sc,typ) = let open Evd in @@ -157,7 +158,7 @@ let pr_meta_map evd = let open Evd in let print_constr = print_kconstr in let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" + Name id -> str"[" ++ Id.print id ++ str"]" | _ -> mt() in let pr_meta_binding = function | (mv,Cltyp (na,b)) -> @@ -177,23 +178,23 @@ let pr_decl (decl,ok) = let open NamedDecl in let print_constr = print_kconstr in match decl with - | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + | 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 "}") let pr_evar_source = function - | Evar_kinds.NamedHole id -> pr_id id + | Evar_kinds.NamedHole id -> Id.print id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> str "subterm of pattern-matching return predicate" - | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id + | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let open Globnames in let print_constr = print_kconstr in let id = Option.get ido in - str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ + str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ spc () ++ print_constr (printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> @@ -202,10 +203,9 @@ let pr_evar_source = function | 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 " ++ pr_id id + | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id | Evar_kinds.SubEvar evk -> - let open Evd in - str "subterm of " ++ str (string_of_existential evk) + str "subterm of " ++ Evar.print evk let pr_evar_info evi = let open Evd in @@ -288,6 +288,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 pr_evar_universe_context ctx = let open UState in @@ -355,7 +356,7 @@ let pr_evar_map_gen with_univs pr_evars sigma = let pr_evar_list sigma l = let open Evd in let pr (ev, evi) = - h 0 (str (string_of_existential ev) ++ + h 0 (Evar.print ev ++ str "==" ++ pr_evar_info evi ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" @@ -434,7 +435,7 @@ let pr_var_decl env decl = (str" := " ++ pb ++ cut () ) in let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in - (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) + (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in @@ -448,7 +449,7 @@ let pr_rel_decl env decl = let ptyp = print_constr_env env Evd.empty (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 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) let print_named_context env = hv 0 (fold_named_context @@ -798,7 +799,7 @@ let fold_constr_with_binders sigma g f n acc c = let iter_constr_with_full_binders g f l c = let open RelDecl in - match kind_of_term c with + match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_, t) -> f l c; f l t @@ -983,9 +984,9 @@ let isMetaOf sigma mv c = match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false let rec subst_meta bl c = - match kind_of_term c with + match kind c with | Meta i -> (try Int.List.assoc i bl with Not_found -> c) - | _ -> map_constr (subst_meta bl) c + | _ -> Constr.map (subst_meta bl) c let rec strip_outer_cast sigma c = match EConstr.kind sigma c with | Cast (c,_,_) -> strip_outer_cast sigma c |