diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 156 |
1 files changed, 80 insertions, 76 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 0c673fbd..7f5087a8 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) open Pp open Util @@ -20,7 +20,6 @@ open Global open Declare open Libnames open Nametab -open Ppconstr open Evd open Proof_type open Decl_mode @@ -30,11 +29,11 @@ open Ppconstr open Constrextern open Tacexpr -let emacs_str s alts = +let emacs_str s alts = match !Flags.print_emacs, !Flags.print_emacs_safechar with | true, true -> alts | true , false -> s - | false,_ -> "" + | false,_ -> "" (**********************************************************************) (** Terms *) @@ -59,6 +58,19 @@ let pr_constr t = pr_constr_env (Global.env()) t let pr_open_lconstr (_,c) = pr_lconstr c let pr_open_constr (_,c) = pr_constr c +let pr_constr_under_binders_env_gen pr env (ids,c) = + (* Warning: clashes can occur with variables of same name in env but *) + (* we also need to preserve the actual names of the patterns *) + (* So what to do? *) + let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in + pr (push_rels_assum assums env) c + +let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env +let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env + +let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c +let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c + let pr_type_core at_top env t = pr_constr_expr (extern_type at_top env t) let pr_ltype_core at_top env t = @@ -78,7 +90,7 @@ let pr_ljudge j = pr_ljudge_env (Global.env()) j let pr_lrawconstr_env env c = pr_lconstr_expr (extern_rawconstr (vars_of_env env) c) -let pr_rawconstr_env env c = +let pr_rawconstr_env env c = pr_constr_expr (extern_rawconstr (vars_of_env env) c) let pr_lrawconstr c = @@ -115,10 +127,7 @@ let pr_inductive env ind = pr_lconstr_env env (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) let pr_evaluable_reference ref = - let ref' = match ref with - | EvalConstRef const -> ConstRef const - | EvalVarRef sp -> VarRef sp in - pr_global ref' + pr_global (Tacred.global_of_evaluable_reference ref) (*let pr_rawterm t = pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*) @@ -134,7 +143,7 @@ let pr_var_decl env (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = pr_lconstr_env env c in let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in @@ -146,7 +155,7 @@ let pr_rel_decl env (na,c,typ) = let pbody = match c with | None -> mt () | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = pr_lconstr_env env c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in @@ -166,7 +175,7 @@ let pr_named_context_of env = let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) -let pr_named_context env ne_context = +let pr_named_context env ne_context = hv 0 (Sign.fold_named_context (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d) ne_context ~init:(mt ())) @@ -183,14 +192,14 @@ let pr_context_unlimited env = fold_named_context (fun env d pps -> let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt)) - env ~init:(mt ()) + env ~init:(mt ()) in let db_env = fold_rel_context (fun env d pps -> let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) env ~init:(mt ()) - in + in (sign_env ++ db_env) let pr_ne_context_of header env = @@ -201,21 +210,21 @@ let pr_ne_context_of header env = let pr_context_limit n env = let named_context = Environ.named_context env in let lgsign = List.length named_context in - if n >= lgsign then + if n >= lgsign then pr_context_unlimited env else let k = lgsign-n in let _,sign_env = fold_named_context (fun env d (i,pps) -> - if i < k then + if i < k then (i+1, (pps ++str ".")) else let pidt = pr_var_decl env d in (i+1, (pps ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pidt))) - env ~init:(0,(mt ())) + env ~init:(0,(mt ())) in let db_env = fold_rel_context @@ -225,10 +234,10 @@ let pr_context_limit n env = str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pnat)) env ~init:(mt ()) - in + in (sign_env ++ db_env) -let pr_context_of env = match Flags.print_hyps_limit () with +let pr_context_of env = match Flags.print_hyps_limit () with | None -> hv 0 (pr_context_unlimited env) | Some n -> hv 0 (pr_context_limit n env) @@ -238,33 +247,33 @@ let pr_restricted_named_context among env = hv 0 (fold_named_context (fun env ((id,_,_) as d) pps -> if true || Idset.mem id among then - pps ++ + pps ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pr_var_decl env d - else + else pps) env ~init:(mt ())) -let pr_predicate pr_elt (b, elts) = +let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then - str"all" ++ + str"all" ++ (if elts = [] then mt () else str" except: " ++ pr_elts) else if elts = [] then str"none" else pr_elts - + let pr_cpred p = pr_predicate pr_con (Cpred.elements p) let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p) -let pr_transparent_state (ids, csts) = +let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) let pr_subgoal_metas metas env= - let pr_one (meta,typ) = - str "?" ++ int meta ++ str " : " ++ - hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ + let pr_one (meta,typ) = + str "?" ++ int meta ++ str " : " ++ + hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") in hv 0 (prlist_with_sep mt pr_one metas) @@ -276,9 +285,9 @@ let default_pr_goal g = mt (), mt (), pr_context_of env, pr_ltype_env_at_top env g.evar_concl - else + else (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - (str"thesis := " ++ fnl ()), + (str "thesis := " ++ fnl ()), pr_context_of env, pr_ltype_env_at_top env g.evar_concl in @@ -287,7 +296,7 @@ let default_pr_goal g = str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () - + (* display the conclusion of a goal *) let pr_concl n g = let env = evar_env g in @@ -296,13 +305,13 @@ let pr_concl n g = str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) -let pr_evgl_sign gl = +let pr_evgl_sign gl = let ps = pr_named_context_of (evar_unfiltered_env gl) in let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in let ids = List.rev (List.map pi1 l) in let warn = if ids = [] then mt () else - (str "(" ++ prlist_with_sep pr_coma pr_id ids ++ str " cannot be used)") + (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in let pc = pr_lconstr gl.evar_concl in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn) @@ -311,10 +320,10 @@ let pr_evgl_sign gl = let rec pr_evars_int i = function | [] -> (mt ()) | (ev,evd)::rest -> - let pegl = pr_evgl_sign evd in + let pegl = pr_evgl_sign evd in let pei = pr_evars_int (i+1) rest in (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - str (string_of_existential ev) ++ str " : " ++ pegl)) ++ + str (string_of_existential ev) ++ str " : " ++ pegl)) ++ fnl () ++ pei let default_pr_subgoal n = @@ -324,27 +333,27 @@ let default_pr_subgoal n = if p = 1 then let pg = default_pr_goal g in v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) - else + else prrec (p-1) rest - in + in prrec n (* Print open subgoals. Checks for uninstantiated existential variables *) -let default_pr_subgoals close_cmd sigma = function - | [] -> +let default_pr_subgoals close_cmd sigma = function + | [] -> begin match close_cmd with Some cmd -> - (str "Subproof completed, now type " ++ str cmd ++ + (str "Subproof completed, now type " ++ str cmd ++ str "." ++ fnl ()) | None -> - let exl = Evarutil.non_instantiated sigma in - if exl = [] then - (str"Proof completed." ++ fnl ()) + let exl = Evarutil.non_instantiated sigma in + if exl = [] then + (str"Proof completed." ++ fnl ()) else let pei = pr_evars_int 1 exl in (str "No more subgoals but non-instantiated existential " ++ - str "variables :" ++fnl () ++ (hov 0 pei)) + str "variables:" ++ fnl () ++ (hov 0 pei)) end | [g] -> let pg = default_pr_goal g in @@ -355,11 +364,11 @@ let default_pr_subgoals close_cmd sigma = function | g::rest -> let pc = pr_concl n g in let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) + (cut () ++ pc ++ prest) in let pg1 = default_pr_goal g1 in let prest = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () + v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ prest ++ fnl ()) @@ -390,24 +399,19 @@ let pr_goal x = !printer_pr.pr_goal x (* End abstraction layer *) (**********************************************************************) -let pr_subgoals_of_pfts pfts = - let close_cmd = Decl_mode.get_end_command pfts in - let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in - let sigma = (top_goal_of_pftreestate pfts).sigma in - pr_subgoals close_cmd sigma gls - let pr_open_subgoals () = let pfts = get_pftreestate () in + let gls = fst (frontier (proof_of_pftreestate pfts)) in match focus() with - | 0 -> - pr_subgoals_of_pfts pfts - | n -> - let pf = proof_of_pftreestate pfts in - let gls = fst (frontier pf) in + | 0 -> + let sigma = (top_goal_of_pftreestate pfts).sigma in + let close_cmd = Decl_mode.get_end_command pfts in + pr_subgoals close_cmd sigma gls + | n -> assert (n > List.length gls); - if List.length gls < 2 then + if List.length gls < 2 then pr_subgoal n gls - else + else (* LEM TODO: this way of saying how many subgoals has to be abstracted out*) v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ pr_subgoal n gls) @@ -419,25 +423,25 @@ let pr_nth_open_subgoal n = (* Elementary tactics *) let pr_prim_rule = function - | Intro id -> + | Intro id -> str"intro " ++ pr_id id - + | Cut (b,replace,id,t) -> if b then (* TODO: express "replace" *) (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") else let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ + (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - + | FixRule (f,n,[],_) -> (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> + + | FixRule (f,n,others,j) -> if j<>0 then warning "Unsupported printing of \"fix\""; let rec print_mut = function - | (f,n,ar)::oth -> + | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth | [] -> mt () in (str"fix " ++ pr_id f ++ str"/" ++ int n ++ @@ -453,26 +457,26 @@ let pr_prim_rule = function (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) | [] -> mt () in (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - | Refine c -> + | Refine c -> str(if occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - + | Convert_concl (c,_) -> (str"change " ++ pr_constr c) - + | Convert_hyp (id,None,t) -> (str"change " ++ pr_constr t ++ spc () ++ str"in " ++ pr_id id) | Convert_hyp (id,Some c,t) -> (str"change " ++ pr_constr c ++ spc () ++ str"in " ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") - + | Thin ids -> (str"clear " ++ prlist_with_sep pr_spc pr_id ids) - + | ThinBody ids -> (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) - + | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) @@ -497,7 +501,7 @@ let prterm = pr_lconstr (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -let pr_assumptionset env s = +let pr_assumptionset env s = if (Environ.ContextObjectMap.is_empty s) then str "Closed under the global context" else @@ -506,7 +510,7 @@ let pr_assumptionset env s = let (v,a,o) = r in match t with | Variable id -> ( Some ( - Option.default (fnl ()) v + Option.default (fnl ()) v ++ str (string_of_id id) ++ str " : " ++ pr_ltype typ @@ -536,7 +540,7 @@ let pr_assumptionset env s = ) s (None,None,None) in - let (vars,axioms,opaque) = + let (vars,axioms,opaque) = ( Option.map (fun p -> str "Section Variables:" ++ p) vars , Option.map (fun p -> str "Axioms:" ++ p) axioms , Option.map (fun p -> str "Opaque constants:" ++ p) opaque @@ -550,7 +554,7 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m [] open Typeclasses let pr_instance i = - pr_global (ConstRef (instance_impl i)) + pr_global (instance_impl i) let pr_instance_gmap insts = prlist_with_sep fnl (fun (gr, insts) -> |