diff options
| author | herbelin | 2005-12-26 20:07:21 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-26 20:07:21 +0000 |
| commit | 52f4136ecf452162adb55c8de031b73c97dcdbac (patch) | |
| tree | 8ac0a4c3584025a44067c6a96c6ce9d92ca93e78 /translate | |
| parent | 099fb1b4c5084bb899e4910e42c971cdfa81e1aa (diff) | |
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 763 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 89 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 742 | ||||
| -rw-r--r-- | translate/pptacticnew.mli | 30 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 968 | ||||
| -rw-r--r-- | translate/ppvernacnew.mli | 31 |
6 files changed, 0 insertions, 2623 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml deleted file mode 100644 index 2d6dd5f709..0000000000 --- a/translate/ppconstrnew.ml +++ /dev/null @@ -1,763 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -(*i*) -open Util -open Pp -open Nametab -open Names -open Nameops -open Libnames -open Ppextend -open Topconstr -open Term -open Pattern -(*i*) - -let sep_p = fun _ -> str"." -let sep_v = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" -let sep_bar = fun _ -> spc() ++ str"| " -let pr_tight_coma () = str "," ++ cut () - -let latom = 0 -let lannot = 100 -let lprod = 200 -let llambda = 200 -let lif = 200 -let lletin = 200 -let lfix = 200 -let larrow = 90 -let lcast = 100 -let larg = 9 -let lapp = 10 -let lposint = 0 -let lnegint = 35 (* must be consistent with Notation "- x" *) -let ltop = (200,E) -let lproj = 1 -let lsimple = (1,E) - -let prec_less child (parent,assoc) = - if parent < 0 && child = lprod then true - else - let parent = abs parent in - match assoc with - | E -> (<=) child parent - | L -> (<) child parent - | Prec n -> child<=n - | Any -> true - -let env_assoc_value v env = - try List.nth env (v-1) - with Not_found -> anomaly ("Inconsistent environment for pretty-print rule") - -let decode_constrlist_value = function - | CAppExpl (_,_,l) -> l - | CApp (_,_,l) -> List.map fst l - | _ -> anomaly "Ill-formed list argument of notation" - -let decode_patlist_value = function - | CPatCstr (_,_,l) -> l - | _ -> anomaly "Ill-formed list argument of notation" - -open Notation - -let rec print_hunk n decode pr env = function - | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env) - | UnpListMetaVar (e,prec,sl) -> - prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl) - (pr (n,prec)) (decode (env_assoc_value e env)) - | UnpTerminal s -> str s - | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub) - | UnpCut cut -> ppcmd_of_cut cut - -let pr_notation_gen decode pr s env = - let unpl, level = find_notation_printing_rule s in - prlist (print_hunk level decode pr env) unpl, level - -let pr_notation = pr_notation_gen decode_constrlist_value -let pr_patnotation = pr_notation_gen decode_patlist_value - -let pr_delimiters key strm = - strm ++ str ("%"^key) - -let surround p = hov 1 (str"(" ++ p ++ str")") - -let pr_located pr ((b,e),x) = - if Options.do_translate() && (b,e)<>dummy_loc then - let (b,e) = unloc (b,e) in - comment b ++ pr x ++ comment e - else pr x - -let pr_com_at n = - if Options.do_translate() && n <> 0 then comment n - else mt() - -let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) - -let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) - -open Rawterm - -let pr_opt pr = function - | None -> mt () - | Some x -> spc() ++ pr x - -let pr_optc pr = function - | None -> mt () - | Some x -> pr_sep_com spc pr x - -let pr_universe = Univ.pr_uni - -let pr_sort = function - | RProp Term.Null -> str "Prop" - | RProp Term.Pos -> str "Set" - | RType u -> str "Type" ++ pr_opt pr_universe u - -let pr_expl_args pr (a,expl) = - match expl with - | None -> pr (lapp,L) a - | Some (_,ExplByPos n) -> - anomaly("Explicitation by position not implemented") - | Some (_,ExplByName id) -> - str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" - -let pr_opt_type pr = function - | CHole _ -> mt () - | t -> cut () ++ str ":" ++ pr t - -let pr_opt_type_spc pr = function - | CHole _ -> mt () - | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - -let pr_id = pr_id - -let pr_name = function - | Anonymous -> str"_" - | Name id -> pr_id id - -let pr_lident (b,_ as loc,id) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) - else pr_id id - -let pr_lname = function - (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna - -let pr_or_var pr = function - | Genarg.ArgArg x -> pr x - | Genarg.ArgVar (loc,s) -> pr_lident (loc,s) - -let las = lapp -let lpator = 100 - -let rec pr_patt sep inh p = - let (strm,prec) = match p with - | CPatAlias (_,p,id) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las - | CPatCstr (_,c,[]) -> pr_reference c, latom - | CPatCstr (_,c,args) -> - pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatAtom (_,None) -> str "_", latom - | CPatAtom (_,Some r) -> pr_reference r, latom - | CPatOr (_,pl) -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator - | CPatNotation (_,"( _ )",[p]) -> - pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env - | CPatNumeral (_,i) -> Bigint.pr_bigint i, latom - | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 - in - let loc = cases_pattern_loc p in - pr_with_comments loc - (sep() ++ if prec_less prec inh then strm else surround strm) - -let pr_patt = pr_patt mt - - -let pr_eqn pr (loc,pl,rhs) = - spc() ++ hov 4 - (pr_with_comments loc - (str "| " ++ - hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++ - pr_sep_com spc (pr ltop) rhs)) - -let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (unloc loc) - | LocalRawAssum((loc,_)::_,_) -> fst (unloc loc) - | _ -> assert false - -let begin_of_binders = function - | b::_ -> begin_of_binder b - | _ -> 0 - -let pr_binder many pr (nal,t) = - match t with - | CHole _ -> prlist_with_sep spc pr_lname nal - | _ -> - let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in - hov 1 (if many then surround s else s) - -let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,t) -> - pr_binder true pr_c (nal,t) - | LocalRawDef (na,c) -> - let c,topt = match c with - | CCast(_,c,_,t) -> c, t - | _ -> c, CHole dummy_loc in - hov 1 (surround - (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c)) - -let pr_undelimited_binders pr_c = - prlist_with_sep spc (pr_binder_among_many pr_c) - -let pr_delimited_binders kw pr_c bl = - let n = begin_of_binders bl in - match bl with - | [LocalRawAssum (nal,t)] -> - pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t) - | LocalRawAssum _ :: _ as bdl -> - pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl - | _ -> assert false - -let pr_let_binder pr x a = - hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ - pr_sep_com (fun () -> brk(0,1)) (pr ltop) a) - -let rec extract_prod_binders = function -(* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) - | CProdN (loc,[],c) -> - extract_prod_binders c - | CProdN (loc,(nal,t)::bl,c) -> - let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,t) :: bl, c - | c -> [], c - -let rec extract_lam_binders = function -(* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) - | CLambdaN (loc,[],c) -> - extract_lam_binders c - | CLambdaN (loc,(nal,t)::bl,c) -> - let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,t) :: bl, c - | c -> [], c - -let pr_global vars ref = pr_global_env vars ref - -let split_lambda = function - | CLambdaN (loc,[[na],t],c) -> (na,t,c) - | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) - | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c)) - | _ -> anomaly "ill-formed fixpoint body" - -let rename na na' t c = - match (na,na') with - | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - -let split_product na' = function - | CArrow (loc,t,c) -> (na',t,c) - | CProdN (loc,[[na],t],c) -> rename na na' t c - | CProdN (loc,([na],t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) - | CProdN (loc,(na::nal,t)::bl,c) -> - rename na na' t (CProdN(loc,(nal,t)::bl,c)) - | _ -> anomaly "ill-formed fixpoint body" - -let merge_binders (na1,ty1) cofun (na2,ty2) codom = - let na = - match snd na1, snd na2 with - Anonymous, Name id -> - if occur_var_constr_expr id cofun then - failwith "avoid capture" - else na2 - | Name id, Anonymous -> - if occur_var_constr_expr id codom then - failwith "avoid capture" - else na1 - | Anonymous, Anonymous -> na1 - | Name id1, Name id2 -> - if id1 <> id2 then failwith "not same name" else na1 in - let ty = - match ty1, ty2 with - CHole _, _ -> ty2 - | _, CHole _ -> ty1 - | _ -> - Constrextern.check_same_type ty1 ty2; - ty2 in - (LocalRawAssum ([na],ty), codom) - -let rec strip_domain bvar cofun c = - match c with - | CArrow(loc,a,b) -> - merge_binders bvar cofun ((dummy_loc,Anonymous),a) b - | CProdN(loc,[([na],ty)],c') -> - merge_binders bvar cofun (na,ty) c' - | CProdN(loc,([na],ty)::bl,c') -> - merge_binders bvar cofun (na,ty) (CProdN(loc,bl,c')) - | CProdN(loc,(na::nal,ty)::bl,c') -> - merge_binders bvar cofun (na,ty) (CProdN(loc,(nal,ty)::bl,c')) - | _ -> failwith "not a product" - -(* Note: binder sharing is lost *) -let rec strip_domains (nal,ty) cofun c = - match nal with - [] -> assert false - | [na] -> - let bnd, c' = strip_domain (na,ty) cofun c in - ([bnd],None,c') - | na::nal -> - let f = CLambdaN(dummy_loc,[(nal,ty)],cofun) in - let bnd, c1 = strip_domain (na,ty) f c in - (try - let bl, rest, c2 = strip_domains (nal,ty) cofun c1 in - (bnd::bl, rest, c2) - with Failure _ -> ([bnd],Some (nal,ty), c1)) - -(* Re-share binders *) -let rec factorize_binders = function - | ([] | [_] as l) -> l - | LocalRawAssum (nal,ty) as d :: (LocalRawAssum (nal',ty')::l as l') -> - (try - let _ = Constrextern.check_same_type ty ty' in - factorize_binders (LocalRawAssum (nal@nal',ty)::l) - with _ -> - d :: factorize_binders l') - | d :: l -> d :: factorize_binders l - -(* Extract lambdas when a type constraint occurs *) -let rec extract_def_binders c ty = - match c with - | CLambdaN(loc,bvar::lams,b) -> - (try - let f = CLambdaN(loc,lams,b) in - let bvar', rest, ty' = strip_domains bvar f ty in - let c' = - match rest, lams with - None,[] -> b - | None, _ -> f - | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in - let (bl,c2,ty2) = extract_def_binders c' ty' in - (factorize_binders (bvar'@bl), c2, ty2) - with Failure _ -> - ([],c,ty)) - | _ -> ([],c,ty) - -let rec split_fix n typ def = - if n = 0 then ([],typ,def) - else - let (na,_,def) = split_lambda def in - let (na,t,typ) = split_product na typ in - let (bl,typ,def) = split_fix (n-1) typ def in - (LocalRawAssum ([na],t)::bl,typ,def) - -let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = - let pr_body = - if dangling_with_for then pr_dangling else pr in - pr_id id ++ str" " ++ - hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++ - pr_opt_type_spc pr t ++ str " :=" ++ - pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c - -let pr_fixdecl pr prd dangling_with_for (id,n,bl,t,c) = - let annot = - let ids = names_of_local_assums bl in - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" - else mt() in - pr_recursive_decl pr prd dangling_with_for id bl annot t c - -let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) = - pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c - -let pr_recursive pr_decl id = function - | [] -> anomaly "(co)fixpoint with no definition" - | [d1] -> pr_decl false d1 - | dl -> - prlist_with_sep (fun () -> fnl() ++ str "with ") - (pr_decl true) dl ++ - fnl() ++ str "for " ++ pr_id id - -let pr_arg pr x = spc () ++ pr x - -let is_var id = function - | CRef (Ident (_,id')) when id=id' -> true - | _ -> false - -let tm_clash = function - | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) - when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false) - nal - -> Some id - | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) - when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false) - nal - -> Some id - | _ -> None - -let pr_case_item pr (tm,(na,indnalopt)) = - hov 0 (pr (lcast,E) tm ++ -(* - (match na with - | Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id - | Anonymous when tm_clash (tm,indnalopt) <> None -> - (* hide [tm] name to avoid conflicts *) - spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*) - | _ -> mt ()) ++ -*) - (match na with (* Decision of printing "_" or not moved to constrextern.ml *) - | Some na -> spc () ++ str "as " ++ pr_name na - | None -> mt ()) ++ - (match indnalopt with - | None -> mt () -(* - | Some (_,ind,nal) -> - spc () ++ str "in " ++ - hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal)) -*) - | Some t -> spc () ++ str "in " ++ pr lsimple t)) - -let pr_case_type pr po = - match po with - | None | Some (CHole _) -> mt() - | Some p -> - spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p) - -let pr_return_type pr po = pr_case_type pr po - -let pr_simple_return_type pr na po = - (match na with - | Some (Name id) -> - spc () ++ str "as " ++ pr_id id - | _ -> mt ()) ++ - pr_case_type pr po - -let pr_proj pr pr_app a f l = - hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") - -let pr_appexpl pr f l = - hov 2 ( - str "@" ++ pr_reference f ++ - prlist (pr_sep_com spc (pr (lapp,L))) l) - -let pr_app pr a l = - hov 2 ( - pr (lapp,L) a ++ - prlist (fun a -> spc () ++ pr_expl_args pr a) l) - -let rec pr sep inherited a = - let (strm,prec) = match a with - | CRef r -> pr_reference r, latom - | CFix (_,id,fix) -> - hov 0 (str"fix " ++ - pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) fix), - lfix - | CCoFix (_,id,cofix) -> - hov 0 (str "cofix " ++ - pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) cofix), - lfix - | CArrow (_,a,b) -> - hov 0 (pr mt (larrow,L) a ++ str " ->" ++ - pr (fun () ->brk(1,0)) (-larrow,E) b), - larrow - | CProdN _ -> - let (bl,a) = extract_prod_binders a in - hov 0 ( - hov 2 (pr_delimited_binders (fun () -> str"forall" ++ spc()) - (pr mt ltop) bl) ++ - str "," ++ pr spc ltop a), - lprod - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in - hov 0 ( - hov 2 (pr_delimited_binders (fun () -> str"fun" ++ spc()) - (pr mt ltop) bl) ++ - - str " =>" ++ pr spc ltop a), - llambda - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) - when x=x' -> - hv 0 ( - hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++ - pr spc ltop b), - lletin - | CLetIn (_,x,a,b) -> - hv 0 ( - hov 2 (str "let " ++ pr_lname x ++ str " :=" ++ - pr spc ltop a ++ str " in") ++ - pr spc ltop b), - lletin - | CAppExpl (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in - let p = pr_proj (pr mt) pr_appexpl c f l1 in - if l2<>[] then - p ++ prlist (pr spc (lapp,L)) l2, lapp - else - p, lproj - | CAppExpl (_,(None,Ident (_,var)),[t]) - | CApp (_,(_,CRef(Ident(_,var))),[t,None]) - when var = Topconstr.ldots_var -> - hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg - | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp - | CApp (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in - assert (snd c = None); - let p = pr_proj (pr mt) pr_app (fst c) f l1 in - if l2<>[] then - p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp - else - p, lproj - | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp - | CCases (_,rtntypopt,c,eqns) -> - v 0 - (hv 0 (str "match" ++ brk (1,2) ++ - hov 0 ( - prlist_with_sep sep_v - (pr_case_item (pr_dangling_with_for mt)) c - ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++ - spc () ++ str "with") ++ - prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), - latom - | CLetTuple (_,nal,(na,po),c,b) -> - hv 0 ( - str "let " ++ - hov 0 (str "(" ++ - prlist_with_sep sep_v pr_name nal ++ - str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ str " in") ++ - pr spc ltop b), - lletin - | CIf (_,c,(na,po),b1,b2) -> - (* On force les parenthèses autour d'un "if" sous-terme (même si le - parsing est lui plus tolérant) *) - hv 0 ( - hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++ - spc () ++ - hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++ - hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), - lif - - | CHole _ -> str "_", latom - | CEvar (_,n) -> str (Evd.string_of_existential n), latom - | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom - | CSort (_,s) -> pr_sort s, latom - | CCast (_,a,_,b) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), - lcast - | CNotation (_,"( _ )",[t]) -> - pr (fun()->str"(") (max_int,L) t ++ str")", latom - | CNotation (_,s,env) -> pr_notation (pr mt) s env - | CNumeral (_,p) -> - Bigint.pr_bigint p, - (if Bigint.is_pos_or_zero p then lposint else lnegint) - | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 - | CDynamic _ -> str "<dynamic>", latom - in - let loc = constr_loc a in - pr_with_comments loc - (sep() ++ if prec_less prec inherited then strm else surround strm) - -and pr_dangling_with_for sep inherited a = - match a with - | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a - | _ -> pr sep inherited a - -let pr = pr mt - -let rec abstract_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl - (abstract_constr_expr c bl) - -let rec prod_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],t,b)) idl - (prod_constr_expr c bl) - -let rec strip_context n iscast t = - if n = 0 then - [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t - else match t with - | CLambdaN (loc,(nal,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CLambdaN (loc,bll,c)) in - LocalRawAssum (nal,t) :: bl', c - | CProdN (loc,(nal,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,t)], CProdN (loc,(nal2,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CProdN (loc,bll,c)) in - LocalRawAssum (nal,t) :: bl', c - | CArrow (loc,t,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawAssum ([loc,Anonymous],t) :: bl', c - | CCast (_,c,_,_) -> strip_context n false c - | CLetIn (_,na,b,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawDef (na,b) :: bl', c - | _ -> anomaly "ppconstrnew: strip_context" - -let pr_constr_env env c = pr lsimple c -let pr_lconstr_env env c = pr ltop c -let pr_constr c = pr_constr_env (Global.env()) c -let pr_lconstr c = pr_lconstr_env (Global.env()) c - -let pr_binders = pr_undelimited_binders (pr ltop) - -let pr_lconstr_env_n env iscast bl c = bl, pr ltop c -let pr_type c = pr ltop c - -let transf_pattern env c = - if Options.do_translate() then - Constrextern.extern_rawconstr (Termops.vars_of_env env) - (Constrintern.for_grammar - (Constrintern.intern_gen false ~allow_soapp:true Evd.empty env) c) - else c - -let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c) - -let pr_rawconstr_env env c = - pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) -let pr_lrawconstr_env env c = - pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) - -let pr_cases_pattern = pr_patt ltop - -let pr_pattern_occ prc = function - ([],c) -> prc c - | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - -let pr_unfold_occ pr_ref = function - ([],qid) -> pr_ref qid - | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - -let pr_qualid qid = str (string_of_qualid qid) - -open Rawterm - -let pr_arg pr x = spc () ++ pr x - -let pr_red_flag pr r = - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rIota then pr_arg str "iota" else mt ()) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if r.rConst = [] then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - -open Genarg - -let pr_metaid id = str"?" ++ pr_id id - -let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function - | Red false -> str "red" - | Hnf -> str "hnf" - | Simpl o -> str "simpl" ++ pr_opt (pr_pattern_occ pr_constr) o - | Cbv f -> - if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then - str "compute" - else - hov 1 (str "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> - hov 1 (str "lazy" ++ pr_red_flag pr_ref f) - | Unfold l -> - hov 1 (str "unfold" ++ spc() ++ - prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l) - | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> - hov 1 (str "pattern" ++ - pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l) - - | Red true -> error "Shouldn't be accessible from user" - | ExtraRedExpr s -> str s - | CbvVm -> str "vm_compute" - -let rec pr_may_eval test prc prlc pr2 = function - | ConstrEval (r,c) -> - hov 0 - (str "eval" ++ brk (1,1) ++ - pr_red_expr (prc,prlc,pr2) r ++ - str " in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> - hov 0 - (str "context " ++ pr_id id ++ spc () ++ - str "[" ++ prlc c ++ str "]") - | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c) - | ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")") - | ConstrTerm c -> prc c - -let pr_may_eval a = pr_may_eval (fun _ -> false) a - -(* Printing reference with translation *) - -let pr_reference r = - let loc = loc_of_reference r in - try match Nametab.extended_locate (snd (qualid_of_reference r)) with - | TrueGlobal ref -> - pr_with_comments loc - (pr_reference (Constrextern.extern_reference loc Idset.empty ref)) - | SyntacticDef kn -> - let is_coq_root d = - let d = repr_dirpath d in - d <> [] & string_of_id (list_last d) = "Coq" in - let dir,id = repr_path (sp_of_syntactic_definition kn) in - let r = - if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then - (match Syntax_def.search_syntactic_definition loc kn with - | RRef (_,ref) -> - Constrextern.extern_reference dummy_loc Idset.empty ref - | _ -> r) - else r - in pr_with_comments loc (pr_reference r) - with Not_found -> - error_global_not_found (snd (qualid_of_reference r)) - -(** constr printers *) - -let pr_term_env env c = pr lsimple (Constrextern.extern_constr false env c) -let pr_lterm_env env c = pr ltop (Constrextern.extern_constr false env c) -let pr_term c = pr_term_env (Global.env()) c -let pr_lterm c = pr_lterm_env (Global.env()) c - -let pr_constr_pattern_env env c = - pr lsimple (Constrextern.extern_pattern env Termops.empty_names_context c) - -let pr_constr_pattern t = - pr lsimple - (Constrextern.extern_pattern (Global.env()) Termops.empty_names_context t) diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli deleted file mode 100644 index 67cb51b5af..0000000000 --- a/translate/ppconstrnew.mli +++ /dev/null @@ -1,89 +0,0 @@ - -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Pp -open Environ -open Term -open Libnames -open Pcoq -open Rawterm -open Topconstr -open Names -open Util -open Genarg - -val extract_lam_binders : - constr_expr -> local_binder list * constr_expr -val extract_prod_binders : - constr_expr -> local_binder list * constr_expr -val extract_def_binders : - constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr -val split_fix : - int -> constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr -val pr_binders : local_binder list -> std_ppcmds - -val prec_less : int -> int * Ppextend.parenRelation -> bool - -val pr_global : Idset.t -> global_reference -> std_ppcmds - -val pr_tight_coma : unit -> std_ppcmds -val pr_located : - ('a -> std_ppcmds) -> 'a located -> std_ppcmds -val pr_lident : identifier located -> std_ppcmds -val pr_lname : name located -> std_ppcmds - -val pr_with_comments : loc -> std_ppcmds -> std_ppcmds -val pr_com_at : int -> std_ppcmds -val pr_sep_com : - (unit -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - constr_expr -> std_ppcmds -val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds -val pr_id : identifier -> std_ppcmds -val pr_name : name -> std_ppcmds -val pr_qualid : qualid -> std_ppcmds -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds -val pr_metaid : identifier -> std_ppcmds -val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> - ('a,'b) red_expr_gen -> std_ppcmds - -val pr_sort : rawsort -> std_ppcmds -val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds -val pr_constr : constr_expr -> std_ppcmds -val pr_lconstr : constr_expr -> std_ppcmds -val pr_constr_env : env -> constr_expr -> std_ppcmds -val pr_lconstr_env : env -> constr_expr -> std_ppcmds -val pr_type : constr_expr -> std_ppcmds -val pr_cases_pattern : cases_pattern_expr -> std_ppcmds -val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval - -> std_ppcmds -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr - - -val pr_rawconstr_env : env -> rawconstr -> std_ppcmds -val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds - -val pr_reference : reference -> std_ppcmds - -(** constr printers *) - -val pr_term_env : env -> constr -> std_ppcmds -val pr_lterm_env : env -> constr -> std_ppcmds -val pr_term : constr -> std_ppcmds -val pr_lterm : constr -> std_ppcmds - -val pr_constr_pattern_env : env -> Pattern.constr_pattern -> std_ppcmds -val pr_constr_pattern : Pattern.constr_pattern -> std_ppcmds diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml deleted file mode 100644 index 64a960417e..0000000000 --- a/translate/pptacticnew.ml +++ /dev/null @@ -1,742 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pp -open Names -open Nameops -open Environ -open Util -open Ppextend -open Ppconstrnew -open Tacexpr -open Rawterm -open Topconstr -open Genarg -open Libnames -open Pptactic - -let sep_v = fun _ -> str"," ++ spc() - -let strip_prod_binders_expr n ty = - let rec strip_ty acc n ty = - match ty with - Topconstr.CProdN(_,bll,a) -> - let nb = - List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in - if nb >= n then (List.rev (bll@acc), a) - else strip_ty (bll@acc) (n-nb) a - | Topconstr.CArrow(_,a,b) -> - if n=1 then - (List.rev (([(dummy_loc,Anonymous)],a)::acc), b) - else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in - strip_ty [] n ty - - -(* In new syntax only double quote char is escaped by repeating it *) -let rec escape_string s = - let rec escape_at s i = - if i<0 then s - else if s.[i] == '"' then - let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in - escape_at s' (i-1) - else escape_at s (i-1) in - escape_at s (String.length s - 1) - -let qstring s = str ("\""^escape_string s^"\"") -let qsnew = qstring - -let pr_ltac_or_var pr = function - | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) - -let pr_arg pr x = spc () ++ pr x - -let pr_ltac_constant sp = - pr_qualid (Nametab.shortest_qualid_of_tactic sp) - -let pr_evaluable_reference_env env = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> - Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) - -let pr_inductive env ind = - Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind) - -let pr_quantified_hypothesis = function - | AnonHyp n -> int n - | NamedHyp id -> pr_id id - -let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h - -let pr_esubst prc l = - let pr_qhyp = function - (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,NamedHyp id,c) -> - str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" - in - prlist_with_sep spc pr_qhyp l - -let pr_bindings_gen for_ex prlc prc = function - | ImplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++ - prlist_with_sep spc prc l) - | ExplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else str "with" ++ spc ()) ++ - pr_esubst prlc l) - | NoBindings -> mt () - -let pr_bindings prlc prc = pr_bindings_gen false prlc prc - -let pr_with_bindings prlc prc (c,bl) = - hov 1 (prc c ++ pr_bindings prlc prc bl) - -let pr_with_constr prc = function - | None -> mt () - | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) - -(* Translator copy of pr_intro_pattern based on a translating "pr_id" *) -let rec pr_intro_pattern = function - | IntroOrAndPattern pll -> pr_case_intro_pattern pll - | IntroWildcard -> str "_" - | IntroIdentifier id -> pr_id id -and pr_case_intro_pattern = function - | [_::_ as pl] -> - str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")" - | pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar - (fun l -> hov 0 (prlist_with_sep spc pr_intro_pattern l)) pll) - ++ str "]" - -let pr_with_names = function - | None -> mt () - | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) - -let pr_occs pp = function - [] -> pp - | nl -> hov 1 (pp ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - -let pr_hyp_location pr_id = function - | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs - | id, occs, InHypTypeOnly -> - spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs - | id, occs, InHypValueOnly -> - spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs - -let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) - -let pr_simple_clause pr_id = function - | [] -> mt () - | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) - -let pr_clauses pr_id = function - { onhyps=None; onconcl=true; concl_occs=nl } -> - pr_in (pr_occs (str " *") nl) - | { onhyps=None; onconcl=false } -> pr_in (str " * |-") - | { onhyps=Some l; onconcl=true; concl_occs=nl } -> - pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l - ++ pr_occs (str" |- *") nl) - | { onhyps=Some l; onconcl=false } -> - pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l) - -let pr_clause_pattern pr_id = function - | (None, []) -> mt () - | (glopt,l) -> - str " in" ++ - prlist - (fun (id,nl) -> prlist (pr_arg int) nl - ++ spc () ++ pr_id id) l ++ - pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt - -let pr_induction_arg prc = function - | ElimOnConstr c -> prc c - | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) - | ElimOnAnonHyp n -> int n - -let pr_induction_kind = function - | SimpleInversion -> str "simple inversion" - | FullInversion -> str "inversion" - | FullInversionClear -> str "inversion_clear" - -let pr_lazy lz = if lz then str "lazy " else mt () - -let pr_match_pattern pr_pat = function - | Term a -> pr_pat a - | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]" - | Subterm (Some id,a) -> - str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" - -let pr_match_hyps pr_pat = function - | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp - -let pr_match_rule m pr pr_pat = function - | Pat ([],mp,t) when m -> - pr_match_pattern pr_pat mp ++ - spc () ++ str "=>" ++ brk (1,4) ++ pr t - | Pat (rl,mp,t) -> - prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++ - spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ - str "=>" ++ brk (1,4) ++ pr t - | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - -let pr_funvar = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - -let pr_let_clause k pr = function - | (id,None,t) -> - hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ - pr (TacArg t)) - | (id,Some c,t) -> - hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++ - pr c ++ - str " :=" ++ brk (1,1) ++ pr (TacArg t)) - -let pr_let_clauses pr = function - | hd::tl -> - hv 0 - (pr_let_clause "let " pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl) - | [] -> anomaly "LetIn must declare at least one binding" - -let pr_rec_clause pr (id,(l,t)) = - hov 0 - (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t - -let pr_rec_clauses pr l = - prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l - -let pr_seq_body pr tl = - hv 0 (str "[ " ++ - prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++ - str " ]") - -let pr_hintbases = function - | None -> spc () ++ str "with *" - | Some [] -> mt () - | Some l -> - spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l) - -let pr_autoarg_adding = function - | [] -> mt () - | l -> - spc () ++ str "adding [" ++ - hv 0 (prlist_with_sep spc pr_reference l) ++ str "]" - -let pr_autoarg_destructing = function - | true -> spc () ++ str "destructing" - | false -> mt () - -let pr_autoarg_usingTDB = function - | true -> spc () ++ str "using tdb" - | false -> mt () - -let rec pr_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - -let pr_then () = str ";" - -let ltop = (5,E) -let lseq = 5 -let ltactical = 3 -let lorelse = 2 -let llet = 1 -let lfun = 1 -let labstract = 3 -let lmatch = 1 -let latom = 0 -let lcall = 1 -let leval = 1 -let ltatom = 1 - -let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq - -open Closure - -let make_pr_tac - (pr_tac_level,pr_constr,pr_lconstr,pr_pat, - pr_cst,pr_ind,pr_ref,pr_ident, - pr_extend,strip_prod_binders) = - -let pr_bindings env = - pr_bindings (pr_lconstr env) (pr_constr env) in -let pr_ex_bindings env = - pr_bindings_gen true (pr_lconstr env) (pr_constr env) in -let pr_with_bindings env = - pr_with_bindings (pr_lconstr env) (pr_constr env) in -let pr_eliminator env cb = - str "using" ++ pr_arg (pr_with_bindings env) cb in -let pr_extend env = - pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) in -let pr_red_expr env = - pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) in - -let pr_constrarg env c = spc () ++ pr_constr env c in -let pr_lconstrarg env c = spc () ++ pr_lconstr env c in -let pr_intarg n = spc () ++ int n in - -let pr_binder_fix env (nal,t) = -(* match t with - | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal - | _ ->*) - let s = - prlist_with_sep spc (pr_lname) nal ++ str ":" ++ - pr_lconstr env t in - spc() ++ hov 1 (str"(" ++ s ++ str")") in - -let pr_fix_tac env (id,n,c) = - let rec set_nth_name avoid n = function - (nal,ty)::bll -> - if n <= List.length nal then - match list_chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> - let id = next_ident_away_from (id_of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) - | _ -> assert false - else - let (id,bll') = set_nth_name avoid (n-List.length nal) bll in - (id,(nal,ty)::bll') - | [] -> assert false in - let (bll,ty) = strip_prod_binders n c in - let names = - List.fold_left - (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) - ln nal) - [] bll in - let idarg,bll = set_nth_name names n bll in - let annot = - if List.length names = 1 then mt() - else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in - hov 1 (str"(" ++ pr_id id ++ - prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ - pr_lconstrarg env ty ++ str")") in -(* spc() ++ - hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg - env c) -*) -let pr_cofix_tac env (id,c) = - hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in - - - (* Printing tactics as arguments *) -let rec pr_atom0 env = function - | TacIntroPattern [] -> str "intros" - | TacIntroMove (None,None) -> str "intro" - | TacAssumption -> str "assumption" - | TacAnyConstructor None -> str "constructor" - | TacTrivial (Some []) -> str "trivial" - | TacAuto (None,Some []) -> str "auto" - | TacReflexivity -> str "reflexivity" - | t -> str "(" ++ pr_atom1 env t ++ str ")" - - (* Main tactic printer *) -and pr_atom1 env = function - | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl - | TacSuperAuto _ | TacExtend (_, - ("GTauto"|"GIntuition"|"TSimplif"| - "LinearIntuition"),_) -> - errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0") - | TacExtend (loc,s,l) -> - pr_with_comments loc (pr_extend env 1 s l) - | TacAlias (loc,s,l,_) -> - pr_with_comments loc (pr_extend env 1 s (List.map snd l)) - - (* Basic tactics *) - | TacIntroPattern [] as t -> pr_atom0 env t - | TacIntroPattern (_::_ as p) -> - hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) - | TacIntrosUntil h -> - hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h) - | TacIntroMove (None,None) as t -> pr_atom0 env t - | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1 - | TacIntroMove (ido1,Some id2) -> - hov 1 - (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ - pr_lident id2) - | TacAssumption as t -> pr_atom0 env t - | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c) - | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c) - | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb) - | TacElim (cb,cbo) -> - hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ - pr_opt (pr_eliminator env) cbo) - | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c) - | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb) - | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c) - | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) - | TacMutualFix (id,n,l) -> - hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ - str"with " ++ prlist_with_sep spc (pr_fix_tac env) l) - | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) - | TacMutualCofix (id,l) -> - hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ - str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l) - | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c) - | TacTrueCut (Anonymous,c) -> - hov 1 (str "assert" ++ pr_constrarg env c) - | TacTrueCut (Name id,c) -> - hov 1 (str "assert" ++ spc () ++ - hov 1 (str"(" ++ pr_id id ++ str " :" ++ - pr_lconstrarg env c ++ str")")) - | TacForward (false,na,c) -> - hov 1 (str "assert" ++ spc () ++ - hov 1 (str"(" ++ pr_name na ++ str " :=" ++ - pr_lconstrarg env c ++ str")")) - | TacForward (true,Anonymous,c) -> - hov 1 (str "pose" ++ pr_constrarg env c) - | TacForward (true,Name id,c) -> - hov 1 (str "pose" ++ spc() ++ - hov 1 (str"(" ++ pr_id id ++ str " :=" ++ - pr_lconstrarg env c ++ str")")) - | TacGeneralize l -> - hov 1 (str "generalize" ++ spc () ++ - prlist_with_sep spc (pr_constr env) l) - | TacGeneralizeDep c -> - hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ - pr_constrarg env c) - | TacLetTac (Anonymous,c,cl) -> - hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl - | TacLetTac (Name id,c,cl) -> - hov 1 (str "set" ++ spc () ++ - hov 1 (str"(" ++ pr_id id ++ str " :=" ++ - pr_lconstrarg env c ++ str")") ++ - pr_clauses pr_ident cl) -(* | TacInstantiate (n,c,ConclLocation ()) -> - hov 1 (str "instantiate" ++ spc() ++ - hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg env c ++ str ")" )) - | TacInstantiate (n,c,HypLocation (id,hloc)) -> - hov 1 (str "instantiate" ++ spc() ++ - hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg env c ++ str ")" ) - ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None))) -*) - (* Derived basic tactics *) - | TacSimpleInduction h -> - hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction (h,e,ids) -> - hov 1 (str "induction" ++ spc () ++ - pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ - pr_opt (pr_eliminator env) e) - | TacSimpleDestruct h -> - hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct (h,e,ids) -> - hov 1 (str "destruct" ++ spc () ++ - pr_induction_arg (pr_constr env) h ++ pr_with_names ids ++ - pr_opt (pr_eliminator env) e) - | TacDoubleInduction (h1,h2) -> - hov 1 - (str "double induction" ++ - pr_arg pr_quantified_hypothesis h1 ++ - pr_arg pr_quantified_hypothesis h2) - | TacDecomposeAnd c -> - hov 1 (str "decompose record" ++ pr_constrarg env c) - | TacDecomposeOr c -> - hov 1 (str "decompose sum" ++ pr_constrarg env c) - | TacDecompose (l,c) -> - hov 1 (str "decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_ind env) l - ++ str "]" ++ pr_constrarg env c)) - | TacSpecialize (n,c) -> - hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ - pr_with_bindings env c) - | TacLApply c -> - hov 1 (str "lapply" ++ pr_constrarg env c) - - (* Automation tactics *) - | TacTrivial (Some []) as x -> pr_atom0 env x - | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db) - | TacAuto (None,Some []) as x -> pr_atom0 env x - | TacAuto (n,db) -> - hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db) - | TacDAuto (n,p) -> - hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p) - - (* Context management *) - | TacClear (keep,l) -> - hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++ - prlist_with_sep spc pr_ident l) - | TacClearBody l -> - hov 1 (str "clearbody" ++ spc () ++ prlist_with_sep spc pr_ident l) - | TacMove (b,id1,id2) -> - (* Rem: only b = true is available for users *) - assert b; - hov 1 - (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ - str "after" ++ brk (1,1) ++ pr_ident id2) - | TacRename (id1,id2) -> - hov 1 - (str "rename" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ - str "into" ++ brk (1,1) ++ pr_ident id2) - - (* Constructors *) - | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l) - | TacRight l -> hov 1 (str "right" ++ pr_bindings env l) - | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l) - | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l) - | TacAnyConstructor (Some t) -> - hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t) - | TacAnyConstructor None as t -> pr_atom0 env t - | TacConstructor (n,l) -> - hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l) - - (* Conversion *) - | TacReduce (r,h) -> - hov 1 (pr_red_expr env r ++ - pr_clauses pr_ident h) - | TacChange (occ,c,h) -> - hov 1 (str "change" ++ brk (1,1) ++ - (match occ with - None -> mt() - | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ") - | Some(ocl,c1) -> - hov 1 (pr_constr env c1 ++ spc() ++ - str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++ - str "with ") ++ - pr_constr env c ++ pr_clauses pr_ident h) - - (* Equivalence relations *) - | TacReflexivity as x -> pr_atom0 env x - | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls - | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c - - (* Equality and inversion *) - | TacInversion (DepInversion (k,c,ids),hyp) -> - hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ - pr_quantified_hypothesis hyp ++ - pr_with_names ids ++ pr_with_constr (pr_constr env) c) - | TacInversion (NonDepInversion (k,cl,ids),hyp) -> - hov 1 (pr_induction_kind k ++ spc () ++ - pr_quantified_hypothesis hyp ++ - pr_with_names ids ++ pr_simple_clause pr_ident cl) - | TacInversion (InversionUsing (c,cl),hyp) -> - hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ - spc () ++ str "using" ++ spc () ++ pr_constr env c ++ - pr_simple_clause pr_ident cl) - -in - -let rec pr_tac env inherited tac = - let (strm,prec) = match tac with - | TacAbstract (t,None) -> - str "abstract " ++ pr_tac env (labstract,L) t, labstract - | TacAbstract (t,Some s) -> - hov 0 - (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++ - str "using " ++ pr_id s), - labstract - | TacLetRecIn (l,t) -> - hv 0 - (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++ - fnl () ++ pr_tac env (llet,E) t), - llet - | TacLetIn (llc,u) -> - v 0 - (hv 0 (pr_let_clauses (pr_tac env ltop) llc - ++ str " in") ++ - fnl () ++ pr_tac env (llet,E) u), - llet - | TacMatch (lz,t,lrul) -> - hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with" - ++ prlist - (fun r -> fnl () ++ str "| " ++ - pr_match_rule true (pr_tac env ltop) pr_pat r) - lrul - ++ fnl() ++ str "end"), - lmatch - | TacMatchContext (lz,lr,lrul) -> - hov 0 (pr_lazy lz ++ - str (if lr then "match reverse goal with" else "match goal with") - ++ prlist - (fun r -> fnl () ++ str "| " ++ - pr_match_rule false (pr_tac env ltop) pr_pat r) - lrul - ++ fnl() ++ str "end"), - lmatch - | TacFun (lvar,body) -> -(* let env = List.fold_right (option_fold_right Idset.add) lvar env in*) - hov 2 (str "fun" ++ - prlist pr_funvar lvar ++ str " =>" ++ spc () ++ - pr_tac env (lfun,E) body), - lfun - | TacThens (t,tl) -> - hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++ - pr_seq_body (pr_tac env ltop) tl), - lseq - | TacThen (t1,t2) -> - hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++ - pr_tac env (lseq,L) t2), - lseq - | TacTry t -> - hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t), - ltactical - | TacDo (n,t) -> - hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ - pr_tac env (ltactical,E) t), - ltactical - | TacRepeat t -> - hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t), - ltactical - | TacProgress t -> - hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t), - ltactical - | TacInfo t -> - hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t), - ltactical - | TacOrelse (t1,t2) -> - hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ - pr_tac env (lorelse,E) t2), - lorelse - | TacFail (ArgArg 0,"") -> str "fail", latom - | TacFail (n,s) -> - str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++ - (if s="" then mt() else (spc() ++ qstring s)), latom - | TacFirst tl -> - str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet - | TacSolve tl -> - str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet - | TacId "" -> str "idtac", latom - | TacId s -> str "idtac" ++ (qstring s), latom - | TacAtom (loc,TacAlias (_,s,l,_)) -> - pr_with_comments loc - (pr_extend env (level_of inherited) s (List.map snd l)), - latom - | TacAtom (loc,t) -> - pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom - | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom - | TacArg(ConstrMayEval (ConstrTerm c)) -> - str "constr:" ++ pr_constr env c, latom - | TacArg(ConstrMayEval c) -> - pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval - | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qstring sopt, latom - | TacArg(Integer n) -> int n, latom - | TacArg(TacCall(loc,f,l)) -> - pr_with_comments loc - (hov 1 (pr_ref f ++ spc () ++ - prlist_with_sep spc (pr_tacarg env) l)), - lcall - | TacArg a -> pr_tacarg env a, latom - in - if prec_less prec inherited then strm - else str"(" ++ strm ++ str")" - -and pr_tacarg env = function - | TacDynamic (loc,t) -> - pr_with_comments loc (str ("<dynamic ["^(Dyn.tag t)^"]>")) - | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s)) - | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat - | TacVoid -> str "()" - | Reference r -> pr_ref r - | ConstrMayEval c -> - pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c - | TacFreshId sopt -> str "fresh" ++ pr_opt qstring sopt - | TacExternal (_,com,req,la) -> - str "external" ++ spc() ++ qstring com ++ spc() ++ qstring req ++ - spc() ++ prlist_with_sep spc (pr_tacarg env) la - | (TacCall _|Tacexp _|Integer _) as a -> - str "ltac:" ++ pr_tac env (latom,E) (TacArg a) - -in (pr_tac, pr_match_rule) - -let strip_prod_binders_rawterm n (ty,_) = - let rec strip_ty acc n ty = - if n=0 then (List.rev acc, (ty,None)) else - match ty with - Rawterm.RProd(loc,na,a,b) -> - strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in - strip_ty [] n ty - -let strip_prod_binders_constr n ty = - let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else - match Term.kind_of_term ty with - Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],a)::acc) (n-1) b - | _ -> error "Cannot translate fix tactic: not enough products" in - strip_ty [] n ty - -let drop_env f _env = f - -let rec raw_printers = - (pr_raw_tactic_level, - drop_env Ppconstrnew.pr_constr, - drop_env Ppconstrnew.pr_lconstr, - Ppconstrnew.pr_pattern, - drop_env pr_reference, - drop_env pr_reference, - pr_reference, - pr_or_metaid pr_lident, - Pptactic.pr_raw_extend, - strip_prod_binders_expr) - -and pr_raw_tactic_level env n (t:raw_tactic_expr) = - fst (make_pr_tac raw_printers) env n t - -and pr_raw_match_rule env t = - snd (make_pr_tac raw_printers) env t - -let pr_and_constr_expr pr (c,_) = pr c - -let rec glob_printers = - (pr_glob_tactic_level, - (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env env)), - (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env env)), - (fun c -> Ppconstrnew.pr_constr_pattern_env (Global.env()) c), - (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))), - (fun env -> pr_or_var (pr_inductive env)), - pr_ltac_or_var (pr_located pr_ltac_constant), - pr_lident, - Pptactic.pr_glob_extend, - strip_prod_binders_rawterm) - -and pr_glob_tactic_level env n (t:glob_tactic_expr) = - fst (make_pr_tac glob_printers) env n t - -and pr_glob_match_rule env t = - snd (make_pr_tac glob_printers) env t - -let ((pr_tactic_level:env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) = - make_pr_tac - (pr_glob_tactic_level, - pr_term_env, - pr_lterm_env, - Ppconstrnew.pr_constr_pattern, - pr_evaluable_reference_env, - pr_inductive, - pr_ltac_constant, - pr_id, - Pptactic.pr_extend, - strip_prod_binders_constr) - -let pr_raw_tactic env = pr_raw_tactic_level env ltop -let pr_glob_tactic env = pr_glob_tactic_level env ltop -let pr_tactic env = pr_tactic_level env ltop - -let _ = Tactic_debug.set_tactic_printer - (fun x -> pr_glob_tactic (Global.env()) x) - -let _ = Tactic_debug.set_match_pattern_printer - (fun env hyp -> - pr_match_pattern - (Printer.pr_pattern_env env (Termops.names_of_rel_context env)) hyp) - -let _ = Tactic_debug.set_match_rule_printer - (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) Printer.pr_pattern rl) diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli deleted file mode 100644 index fa959fdb46..0000000000 --- a/translate/pptacticnew.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Pp -open Genarg -open Tacexpr -open Proof_type -open Topconstr -open Names -open Environ -open Ppextend - -val qsnew : string -> std_ppcmds - -val pr_intro_pattern : intro_pattern_expr -> std_ppcmds - -val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds - -val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds - -val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds - -val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml deleted file mode 100644 index ce07001de8..0000000000 --- a/translate/ppvernacnew.ml +++ /dev/null @@ -1,968 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pp -open Names -open Nameops -open Nametab -open Util -open Extend -open Vernacexpr -open Ppconstrnew -open Pptacticnew -open Rawterm -open Genarg -open Pcoq -open Libnames -open Ppextend -open Topconstr -open Decl_kinds -open Tacinterp - -let pr_spc_type = pr_sep_com spc pr_type - -let pr_lident (b,_ as loc,id) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) - else pr_id id - -let string_of_fqid fqid = - String.concat "." (List.map string_of_id fqid) - -let pr_fqid fqid = str (string_of_fqid fqid) - -let pr_lfqid (_,_ as loc,fqid) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) - else - pr_fqid fqid - -let pr_lname = function - (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna - -let pr_ltac_id = Nameops.pr_id - -let pr_module r = - let update_ref s = match r with - | Ident (loc,_) -> - Ident (loc,id_of_string s) - | Qualid (loc,qid) -> - Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in - let dir = - try - Nametab.full_name_module (snd (qualid_of_reference r)) - with _ -> - try - pi2 (Library.locate_qualified_library (snd (qualid_of_reference r))) - with _ -> - errorlabstrm "" (str"Translator cannot find " ++ Libnames.pr_reference r) - in - let r = match List.rev (List.map string_of_id (repr_dirpath dir)) with - | [ "Coq"; "Lists"; "List" ] -> update_ref "MonoList" - | [ "Coq"; "Lists"; "PolyList" ] -> update_ref "List" - | _ -> r in - Libnames.pr_reference r - -let pr_import_module = - (* We assume List is never imported with "Import" ... *) - Libnames.pr_reference - -let pr_reference = Ppconstrnew.pr_reference - -let sep_end () = str"." - -(* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *) -(* -let pr_raw_tactic_env l env t = - Pptacticnew.pr_raw_tactic env t -*) -let pr_raw_tactic_env l env t = - Pptacticnew.pr_glob_tactic env (Tacinterp.glob_tactic_env l env t) - -let pr_gen env t = - Pptactic.pr_raw_generic - Ppconstrnew.pr_constr - Ppconstrnew.pr_lconstr - (Pptacticnew.pr_raw_tactic_level env) pr_reference t - -let pr_raw_tactic tac = - Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac) - -let rec extract_signature = function - | [] -> [] - | Egrammar.TacNonTerm (_,(_,t),_) :: l -> t :: extract_signature l - | _::l -> extract_signature l - -let rec match_vernac_rule tys = function - [] -> raise Not_found - | pargs::rls -> - if extract_signature pargs = tys then pargs - else match_vernac_rule tys rls - -let sep = fun _ -> spc() -let sep_p = fun _ -> str"." -let sep_v = fun _ -> str"," -let sep_v2 = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" - -let pr_ne_sep sep pr = function - [] -> mt() - | l -> sep() ++ pr l - -let pr_entry_prec = function - | Some Gramext.LeftA -> str"LEFTA " - | Some Gramext.RightA -> str"RIGHTA " - | Some Gramext.NonA -> str"NONA " - | None -> mt() - -let pr_prec = function - | Some Gramext.LeftA -> str", left associativity" - | Some Gramext.RightA -> str", right associativity" - | Some Gramext.NonA -> str", no associativity" - | None -> mt() - -let pr_set_entry_type = function - | ETIdent -> str"ident" - | ETReference -> str"global" - | ETPattern -> str"pattern" - | ETConstr _ -> str"constr" - | ETOther (_,e) -> str e - | ETBigint -> str "bigint" - | ETConstrList _ -> failwith "Internal entry type" - -let strip_meta id = - let s = string_of_id id in - if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) - else id - -let pr_production_item = function - | VNonTerm (loc,nt,Some p) -> str nt ++ str"(" ++ pr_id (strip_meta p) ++ str")" - | VNonTerm (loc,nt,None) -> str nt - | VTerm s -> qsnew s - -let pr_comment pr_c = function - | CommentConstr c -> pr_c c - | CommentString s -> qsnew s - | CommentInt n -> int n - -let pr_in_out_modules = function - | SearchInside l -> spc() ++ str"inside" ++ spc() ++ prlist_with_sep sep pr_module l - | SearchOutside [] -> mt() - | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l - -let pr_search_about = function - | SearchRef r -> pr_reference r - | SearchString s -> qsnew s - -let pr_search a b pr_p = match a with - | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b - | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b - -let pr_locality local = if local then str "Local " else str "" - -let pr_explanation imps = function - | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1))) - | ExplByName id -> pr_id id - -let pr_class_rawexpr = function - | FunClass -> str"Funclass" - | SortClass -> str"Sortclass" - | RefClass qid -> pr_reference qid - -let pr_option_ref_value = function - | QualidRefValue id -> pr_reference id - | StringRefValue s -> qsnew s - -let pr_printoption a b = match a with - | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b - | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b - -let pr_set_option a b = - let pr_opt_value = function - | IntValue n -> spc() ++ int n - | StringValue s -> spc() ++ str s - | BoolValue b -> mt() - in pr_printoption a None ++ pr_opt_value b - -let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)" - -let pr_destruct_location = function - | Tacexpr.ConclLocation () -> str"Conclusion" - | Tacexpr.HypLocation b -> if b then str"Discardable Hypothesis" else str"Hypothesis" - -let pr_opt_hintbases l = match l with - | [] -> mt() - | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z - -let pr_hints local db h pr_c pr_pat = - let opth = pr_opt_hintbases db in - let pph = - match h with - | HintsResolve l -> - str "Resolve " ++ - prlist_with_sep sep pr_c (List.map snd l) - | HintsImmediate l -> - str"Immediate" ++ spc() ++ - prlist_with_sep sep pr_c (List.map snd l) - | HintsUnfold l -> - str "Unfold " ++ - prlist_with_sep sep pr_reference (List.map snd l) - | HintsConstructors (n,c) -> - str"Constructors" ++ spc() ++ - prlist_with_sep spc pr_reference c - | HintsExtern (name,n,c,tac) -> - str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++ - spc() ++ pr_raw_tactic tac - | HintsDestruct(name,i,loc,c,tac) -> - str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++ - hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++ - pr_c c ++ str " =>") ++ spc() ++ - pr_raw_tactic tac in - hov 2 (str"Hint "++pr_locality local ++ pph ++ opth) - -let pr_with_declaration pr_c = function - | CWith_Definition (id,c) -> - let p = pr_c c in - str"Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p - | CWith_Module (id,qid) -> - str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_located pr_qualid qid - -let rec pr_module_type pr_c = function - | CMTEident qid -> spc () ++ pr_located pr_qualid qid - | CMTEwith (mty,decl) -> - let m = pr_module_type pr_c mty in - let p = pr_with_declaration pr_c decl in - m ++ spc() ++ str"with" ++ spc() ++ p - -let pr_of_module_type prc (mty,b) = - str (if b then ":" else "<:") ++ - pr_module_type prc mty - -let pr_require_token = function - | Some true -> str "Export " - | Some false -> str "Import " - | None -> mt() - -let pr_module_vardecls pr_c (export,idl,mty) = - let m = pr_module_type pr_c mty in - (* Update the Nametab for interpreting the body of module/modtype *) - let lib_dir = Lib.library_dp() in - List.iter (fun (_,id) -> - Declaremods.process_module_bindings [id] - [make_mbid lib_dir (string_of_id id), - Modintern.interp_modtype (Global.env()) mty]) idl; - (* Builds the stream *) - spc() ++ - hov 1 (str"(" ++ pr_require_token export ++ - prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")") - -let pr_module_binders l pr_c = - (* Effet de bord complexe pour garantir la declaration des noms des - modules parametres dans la Nametab des l'appel de pr_module_binders - malgre l'aspect paresseux des streams *) - let ml = List.map (pr_module_vardecls pr_c) l in - prlist (fun id -> id) ml - -let pr_module_binders_list l pr_c = pr_module_binders l pr_c - -let rec pr_module_expr = function - | CMEident qid -> pr_located pr_qualid qid - | CMEapply (me1,(CMEident _ as me2)) -> - pr_module_expr me1 ++ spc() ++ pr_module_expr me2 - | CMEapply (me1,me2) -> - pr_module_expr me1 ++ spc() ++ - hov 1 (str"(" ++ pr_module_expr me2 ++ str")") - -let pr_type_option pr_c = function - | CHole loc -> mt() - | _ as c -> brk(0,2) ++ str":" ++ pr_c c - -let pr_decl_notation prc = - pr_opt (fun (ntn,c,scopt) -> fnl () ++ - str "where " ++ qsnew ntn ++ str " := " ++ prc c ++ - pr_opt (fun sc -> str ": " ++ str sc) scopt) - -let pr_vbinders l = - hv 0 (pr_binders l) - -let pr_binders_arg = - pr_ne_sep spc pr_binders - -let pr_and_type_binders_arg bl = - pr_binders_arg bl - -let pr_onescheme (id,dep,ind,s) = - hov 0 (pr_lident id ++ str" :=") ++ spc() ++ - hov 0 ((if dep then str"Induction for" else str"Minimality for") - ++ spc() ++ pr_reference ind) ++ spc() ++ - hov 0 (str"Sort" ++ spc() ++ pr_sort s) - -let begin_of_inductive = function - [] -> 0 - | (_,((loc,_),_))::_ -> fst (unloc loc) - -let pr_class_rawexpr = function - | FunClass -> str"Funclass" - | SortClass -> str"Sortclass" - | RefClass qid -> pr_reference qid - -let pr_assumption_token many = function - | (Local,Logical) -> - str (if many then "Hypotheses" else "Hypothesis") - | (Local,Definitional) -> - str (if many then "Variables" else "Variable") - | (Global,Logical) -> - str (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> - str (if many then "Parameters" else "Parameter") - | (Global,Conjectural) -> str"Conjecture" - | (Local,Conjectural) -> - anomaly "Don't know how to translate a local conjecture" - -let pr_params pr_c (xl,(c,t)) = - hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ - (if c then str":>" else str":" ++ - spc() ++ pr_c t)) - -let rec factorize = function - | [] -> [] - | (c,(idl,t))::l -> - match factorize l with - | (xl,t')::l' when t' = (c,t) -> (idl@xl,t')::l' - | l' -> (idl,(c,t))::l' - -let pr_ne_params_list pr_c l = - match factorize l with - | [p] -> pr_params pr_c p - | l -> - prlist_with_sep spc - (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l -(* - prlist_with_sep pr_semicolon (pr_params pr_c) -*) - -let pr_thm_token = function - | Theorem -> str"Theorem" - | Lemma -> str"Lemma" - | Fact -> str"Fact" - | Remark -> str"Remark" - -let pr_syntax_modifier = function - | SetItemLevel (l,NextLevel) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ str"at next level" - | SetItemLevel (l,NumLevel n) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ str"at level" ++ spc() ++ int n - | SetLevel n -> str"at level" ++ spc() ++ int n - | SetAssoc Gramext.LeftA -> str"left associativity" - | SetAssoc Gramext.RightA -> str"right associativity" - | SetAssoc Gramext.NonA -> str"no associativity" - | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ - | SetOnlyParsing -> str"only parsing" - | SetFormat s -> str"format " ++ pr_located qsnew s - -let pr_syntax_modifiers = function - | [] -> mt() - | l -> spc() ++ - hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - -let print_level n = - if n <> 0 then str " (at level " ++ int n ++ str ")" else mt () - -let pr_grammar_tactic_rule n (_,pil,t) = - hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ - hov 0 (prlist_with_sep sep pr_production_item pil ++ - spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) - -let pr_box b = let pr_boxkind = function - | PpHB n -> str"h" ++ spc() ++ int n - | PpVB n -> str"v" ++ spc() ++ int n - | PpHVB n -> str"hv" ++ spc() ++ int n - | PpHOVB n -> str"hov" ++ spc() ++ int n - | PpTB -> str"t" -in str"<" ++ pr_boxkind b ++ str">" - -let pr_paren_reln_or_extern = function - | None,L -> str"L" - | None,E -> str"E" - | Some pprim,Any -> qsnew pprim - | Some pprim,Prec p -> qsnew pprim ++ spc() ++ str":" ++ spc() ++ int p - | _ -> mt() -(* -let rec pr_next_hunks = function - | UNP_FNL -> str"FNL" - | UNP_TAB -> str"TAB" - | RO c -> qsnew c - | UNP_BOX (b,ll) -> str"[" ++ pr_box b ++ prlist_with_sep sep pr_next_hunks ll ++ str"]" - | UNP_BRK (n,m) -> str"[" ++ int n ++ spc() ++ int m ++ str"]" - | UNP_TBRK (n,m) -> str"[ TBRK" ++ int n ++ spc() ++ int m ++ str"]" - | PH (e,None,_) -> print_ast e - | PH (e,Some ext,pr) -> print_ast e ++ spc() ++ str":" ++ spc() ++ pr_paren_reln_or_extern (Some ext,pr) - | UNP_SYMBOLIC _ -> mt() - -let pr_unparsing u = - str "[ " ++ prlist_with_sep sep pr_next_hunks u ++ str " ]" - -let pr_astpat a = str"<<" ++ print_ast a ++ str">>" - -let pr_syntax_rule (nm,s,u) = str nm ++ spc() ++ str"[" ++ pr_astpat s ++ str"]" ++ spc() ++ str"->" ++ spc() ++ pr_unparsing u - -let pr_syntax_entry (p,rl) = - str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++ - prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl -*) -let pr_vernac_solve (i,env,tac,deftac) = - (if i = 1 then mt() else int i ++ str ": ") ++ - Pptacticnew.pr_glob_tactic env tac - ++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt () - with UserError _|Stdpp.Exc_located _ -> mt()) - -(**************************************) -(* Pretty printer for vernac commands *) -(**************************************) -let make_pr_vernac pr_constr pr_lconstr = - -let pr_constrarg c = spc () ++ pr_constr c in -let pr_lconstrarg c = spc () ++ pr_lconstr c in -let pr_intarg n = spc () ++ int n in - -let rec pr_vernac = function - - (* Proof management *) - | VernacAbortAll -> str "Abort All" - | VernacRestart -> str"Restart" - | VernacSuspend -> str"Suspend" - | VernacUnfocus -> str"Unfocus" - | VernacGoal c -> str"Goal" ++ pr_lconstrarg c - | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacResume id -> str"Resume" ++ pr_opt pr_lident id - | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i - | VernacBacktrack (i,j,k) -> - str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] - | VernacFocus i -> str"Focus" ++ pr_opt int i - | VernacGo g -> - let pr_goable = function - | GoTo i -> int i - | GoTop -> str"top" - | GoNext -> str"next" - | GoPrev -> str"prev" - in str"Go" ++ spc() ++ pr_goable g - | VernacShow s -> - let pr_showable = function - | ShowGoal n -> str"Show" ++ pr_opt int n - | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n - | ShowProof -> str"Show Proof" - | ShowNode -> str"Show Node" - | ShowScript -> str"Show Script" - | ShowExistentials -> str"Show Existentials" - | ShowTree -> str"Show Tree" - | ShowProofNames -> str"Show Conjectures" - | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") - | ShowMatch id -> str"Show Match " ++ pr_lident id - | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l - | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l - in pr_showable s - | VernacCheckGuard -> str"Guarded" - | VernacDebug b -> pr_topcmd b - - (* Resetting *) - | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id - | VernacResetInitial -> str"Reset Initial" - | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i - | VernacBackTo i -> str"BackTo" ++ pr_intarg i - - (* State management *) - | VernacWriteState s -> str"Write State" ++ spc () ++ qsnew s - | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s - - (* Control *) - | VernacList l -> - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l - ++ spc() ++ str"]") - | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" - ++ spc()) else spc() ++ qsnew s - | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v - | VernacVar id -> pr_lident id - - (* Syntax *) - | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) - | VernacOpenCloseScope (local,opening,sc) -> - str (if opening then "Open " else "Close ") ++ pr_locality local ++ - str "Scope" ++ spc() ++ str sc - | VernacDelimiters (sc,key) -> - str"Delimit Scope" ++ spc () ++ str sc ++ - spc() ++ str "with " ++ str key - | VernacBindScope (sc,cll) -> - str"Bind Scope" ++ spc () ++ str sc ++ - spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll - | VernacArgumentsScope (q,scl) -> let pr_opt_scope = function - | None -> str"_" - | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *) - hov 0 (hov 0 (str"Infix " ++ pr_locality local - ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++ - pr_syntax_modifiers mv ++ - (match sn with - | None -> mt() - | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) - | VernacNotation (local,c,(s,l),opt) -> - let ps = - let n = String.length s in - if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' - then - let s' = String.sub s 1 (n-2) in - if String.contains s' '\'' then qsnew s else str s' - else qsnew s in - hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++ - str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++ - (match opt with - | None -> mt() - | Some sc -> str" :" ++ spc() ++ str sc)) - | VernacSyntaxExtension (local,(s,l)) -> - str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++ - pr_syntax_modifiers l - - (* Gallina *) - | VernacDefinition (d,id,b,f) -> (* A verifier... *) - let pr_def_token = function - | Local, Coercion -> str"Coercion Local" - | Global, Coercion -> str"Coercion" - | Local, Definition _ -> str"Let" - | Global, Definition b -> - if b then str"Boxed Definition" - else str"Definition" - | Local, SubClass -> str"Local SubClass" - | Global, SubClass -> str"SubClass" - | Global, CanonicalStructure -> str"Canonical Structure" - | Local, CanonicalStructure -> - anomaly "Don't know how to translate a local canonical structure" in - let pr_reduce = function - | None -> mt() - | Some r -> - str"Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++ - str" in" ++ spc() in - let pr_def_body = function - | DefineBody (bl,red,body,d) -> - let ty = match d with - | None -> mt() - | Some ty -> spc() ++ str":" ++ pr_sep_com spc pr_lconstr ty - in - (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) - | ProveBody (bl,t) -> - (pr_binders_arg bl, str" :" ++ pr_spc_type t, None) in - let (binds,typ,c) = pr_def_body b in - hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++ - (match c with - | None -> mt() - | Some cc -> str" :=" ++ spc() ++ cc)) - - | VernacStartTheoremProof (ki,id,(bl,c),b,d) -> - hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++ - (match bl with - | [] -> mt() - | _ -> pr_binders bl ++ spc()) - ++ str":" ++ pr_spc_type c) - | VernacEndProof Admitted -> str"Admitted" - | VernacEndProof (Proved (opac,o)) -> (match o with - | None -> if opac then str"Qed" else str"Defined" - | Some (id,th) -> (match th with - | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id - | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) - | VernacExactProof c -> - hov 2 (str"Proof" ++ pr_lconstrarg c) - | VernacAssumption (stre,l) -> - let n = List.length (List.flatten (List.map fst (List.map snd l))) in - hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_type l) - | VernacInductive (f,l) -> - - let pr_constructor (coe,(id,c)) = - hov 2 (pr_lident id ++ str" " ++ - (if coe then str":>" else str":") ++ - pr_sep_com spc pr_type c) in - let pr_constructor_list l = match l with - | [] -> mt() - | _ -> - pr_com_at (begin_of_inductive l) ++ - fnl() ++ - str (if List.length l = 1 then " " else " | ") ++ - prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind key (id,ntn,indpar,s,lc) = - hov 0 ( - str key ++ spc() ++ - pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ - spc() ++ pr_type s ++ - str" :=") ++ pr_constructor_list lc ++ - pr_decl_notation pr_constr ntn in - - hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) - ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) - - - | VernacFixpoint (recs,b) -> - let name_of_binder = function - | LocalRawAssum (nal,_) -> nal - | LocalRawDef (_,_) -> [] in - let pr_onerec = function - | (id,n,bl,type_,def),ntn -> - let (bl',def,type_) = - if Options.do_translate() then extract_def_binders def type_ - else ([],def,type_) in - let bl = bl @ bl' in - let ids = List.flatten (List.map name_of_binder bl) in - let name = - try snd (List.nth ids n) - with Failure _ -> - warn (str "non-printable fixpoint \""++pr_id id++str"\""); - Anonymous in - let annot = - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name name ++ str"}" - else mt() in - pr_id id ++ pr_binders_arg bl ++ annot ++ spc() - ++ pr_type_option (fun c -> spc() ++ pr_type c) type_ - ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ - pr_decl_notation pr_constr ntn - in - let start = if b then "Boxed Fixpoint" else "Fixpoint" in - hov 1 (str start ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) - - | VernacCoFixpoint (corecs,b) -> - let pr_onecorec (id,bl,c,def) = - let (bl',def,c) = - if Options.do_translate() then extract_def_binders def c - else ([],def,c) in - let bl = bl @ bl' in - pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ - spc() ++ pr_type c ++ - str" :=" ++ brk(1,1) ++ pr_lconstr def in - let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in - hov 1 (str start ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) - | VernacScheme l -> - hov 2 (str"Scheme" ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) - - (* Gallina extensions *) - | VernacRecord (b,(oc,name),ps,s,c,fs) -> - let pr_record_field = function - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_type t) - | (oc,DefExpr(id,b,opt)) -> (match opt with - | Some t -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_type t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) in - hov 2 - (str (if b then "Record" else "Structure") ++ - (if oc then str" > " else str" ") ++ pr_lident name ++ - pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ - str" := " ++ - (match c with - | None -> mt() - | Some sc -> pr_lident sc) ++ - spc() ++ str"{" ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")) - | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) - | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id) - | VernacRequire (exp,spe,l) -> hov 2 - (str "Require" ++ spc() ++ pr_require_token exp ++ - (match spe with - | None -> mt() - | Some flag -> - (if flag then str"Specification" else str"Implementation") ++ - spc ()) ++ - prlist_with_sep sep pr_module l) - | VernacImport (f,l) -> - (if f then str"Export" else str"Import") ++ spc() ++ - prlist_with_sep sep pr_import_module l - | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_reference q - | VernacCoercion (s,id,c1,c2) -> - hov 1 ( - str"Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ - pr_reference id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ - spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - | VernacIdentityCoercion (s,id,c1,c2) -> - hov 1 ( - str"Identity Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ - spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ - spc() ++ pr_class_rawexpr c2) - - (* Modules and Module Types *) - | VernacDefineModule (export,m,bl,ty,bd) -> - let b = pr_module_binders_list bl pr_lconstr in - hov 2 (str"Module" ++ spc() ++ pr_require_token export ++ - pr_lident m ++ b ++ - pr_opt (pr_of_module_type pr_lconstr) ty ++ - pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) - | VernacDeclareModule (export,id,bl,m1) -> - let b = pr_module_binders_list bl pr_lconstr in - hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ - pr_lident id ++ b ++ - pr_of_module_type pr_lconstr m1) - | VernacDeclareModuleType (id,bl,m) -> - let b = pr_module_binders_list bl pr_lconstr in - hov 2 (str"Module Type " ++ pr_lident id ++ b ++ - pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) - - (* Solving *) - | VernacSolve (i,tac,deftac) -> - (* Normally shunted by vernac.ml *) - let env = - try snd (Pfedit.get_goal_context i) - with UserError _ -> Global.env() in - let tac = - Options.with_option Options.translate_syntax - (Constrintern.for_grammar (Tacinterp.glob_tactic_env [] env)) tac in - pr_vernac_solve (i,env,tac,deftac) - - | VernacSolveExistential (i,c) -> - str"Existential " ++ int i ++ pr_lconstrarg c - - (* Auxiliary file and library management *) - | VernacRequireFrom (exp,spe,f) -> hov 2 - (str"Require" ++ spc() ++ pr_require_token exp ++ - (match spe with - | None -> mt() - | Some false -> str"Implementation" ++ spc() - | Some true -> str"Specification" ++ spc ()) ++ - qsnew f) - | VernacAddLoadPath (fl,s,d) -> hov 2 - (str"Add" ++ - (if fl then str" Rec " else spc()) ++ - str"LoadPath" ++ spc() ++ qsnew s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) - | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qsnew s - | VernacAddMLPath (fl,s) -> - str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qsnew s - | VernacDeclareMLModule l -> - hov 2 (str"Declare ML Module" ++ spc() ++ prlist_with_sep sep qsnew l) - | VernacChdir s -> str"Cd" ++ pr_opt qsnew s - - (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> - let pr_tac_body (id, body) = - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - pr_located pr_ltac_id id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ pr_id id) idl - ++ str" :=" ++ brk(1,1) ++ - let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in - pr_raw_tactic_env - (idl @ List.map snd (List.map fst l)) - (Global.env()) - body in - hov 1 - (((*if !Options.p1 then - (if rc then str "Recursive " else mt()) ++ - str "Tactic Definition " else*) - (* Rec by default *) str "Ltac ") ++ - prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) - | VernacHints (local,dbnames,h) -> - pr_hints local dbnames h pr_constr pr_pattern - | VernacSyntacticDefinition (id,c,local,onlyparsing) -> - hov 2 - (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ - pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (q,None) -> - hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) - | VernacDeclareImplicits (q,Some l) -> - let r = Nametab.global q in - Impargs.declare_manual_implicits r l; - let imps = Impargs.implicits_of_global r in - hov 1 (str"Implicit Arguments" ++ spc() ++ pr_reference q ++ spc() ++ - str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]") - | VernacReserve (idl,c) -> - hov 1 (str"Implicit Type" ++ - str (if List.length idl > 1 then "s " else " ") ++ - prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c) - | VernacSetOpacity (fl,l) -> - hov 1 ((if fl then str"Opaque" else str"Transparent") ++ - spc() ++ prlist_with_sep sep pr_reference l) - - | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue true) -> - str"Set Implicit Arguments" - ++ - (if !Options.translate_strict_impargs then - sep_end () ++ fnl () ++ str"Unset Strict Implicit" - else mt ()) - | VernacUnsetOption (Goptions.SecondaryTable ("Implicit","Arguments")) - | VernacSetOption (Goptions.SecondaryTable ("Implicit","Arguments"),BoolValue false) -> - (if !Options.translate_strict_impargs then - str"Set Strict Implicit" ++ sep_end () ++ fnl () - else mt ()) - ++ - str"Unset Implicit Arguments" - - | VernacSetOption (Goptions.SecondaryTable (a,"Implicits"),BoolValue true) -> - str("Set "^a^" Implicit") - | VernacUnsetOption (Goptions.SecondaryTable (a,"Implicits")) -> - str("Unset "^a^" Implicit") - - | VernacUnsetOption na -> - hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) - | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) - | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) - | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) - | VernacPrintOption na -> hov 2 (str"Test" ++ spc() ++ pr_printoption na None) - | VernacCheckMayEval (r,io,c) -> - let pr_mayeval r c = match r with - | Some r0 -> - hov 2 (str"Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++ - spc() ++ str"in" ++ spc () ++ pr_constr c) - | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) - in - (if io = None then mt() else int (out_some io) ++ str ": ") ++ - pr_mayeval r c - | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) - | VernacPrint p -> - let pr_printable = function - | PrintFullContext -> str"Print All" - | PrintSectionContext s -> - str"Print Section" ++ spc() ++ Libnames.pr_reference s - | PrintGrammar (uni,ent) -> - msgerrnl (str "warning: no direct translation of Print Grammar entry"); - str"Print Grammar" ++ spc() ++ str ent - | PrintLoadPath -> str"Print LoadPath" - | PrintModules -> str"Print Modules" - | PrintMLLoadPath -> str"Print ML Path" - | PrintMLModules -> str"Print ML Modules" - | PrintGraph -> str"Print Graph" - | PrintClasses -> str"Print Classes" - | PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_reference qid - | PrintCoercions -> str"Print Coercions" - | PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t - | PrintCanonicalConversions -> str"Print Canonical Structures" - | PrintTables -> str"Print Tables" - | PrintOpaqueName qid -> str"Print Term" ++ spc() ++ pr_reference qid - | PrintHintGoal -> str"Print Hint" - | PrintHint qid -> str"Print Hint" ++ spc() ++ pr_reference qid - | PrintHintDb -> str"Print Hint *" - | PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s - | PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s - | PrintUniverses fopt -> str"Dump Universes" ++ pr_opt str fopt - | PrintName qid -> str"Print" ++ spc() ++ pr_reference qid - | PrintLocalContext -> assert false - (* str"Print" *) - | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid - | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid - | PrintInspect n -> str"Inspect" ++ spc() ++ int n - | PrintSetoids -> str"Print Setoids" - | PrintScopes -> str"Print Scopes" - | PrintScope s -> str"Print Scope" ++ spc() ++ str s - | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s - | PrintAbout qid -> str"About" ++ spc() ++ pr_reference qid - | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid - in pr_printable p - | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern - | VernacLocate loc -> - let pr_locate =function - | LocateTerm qid -> pr_reference qid - | LocateFile f -> str"File" ++ spc() ++ qsnew f - | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid - | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid - | LocateNotation s -> qsnew s - in str"Locate" ++ spc() ++ pr_locate loc - | VernacComments l -> - hov 2 - (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) - | VernacNop -> mt() - - (* Toplevel control *) - | VernacToplevelControl exn -> pr_topcmd exn - - (* For extension *) - | VernacExtend (s,c) -> pr_extend s c - | VernacProof Tacexpr.TacId _ -> str "Proof" - | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te - -and pr_extend s cl = - let pr_arg a = - try pr_gen (Global.env()) a - with Failure _ -> str ("<error in "^s^">") in - try - let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in - let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in - let (pp,_) = - List.fold_left - (fun (strm,args) pi -> - match pi with - Egrammar.TacNonTerm _ -> - (strm ++ pr_gen (Global.env()) (List.hd args), - List.tl args) - | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) - (mt(),cl) rl in - hov 1 pp - with Not_found -> - hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")") - -in pr_vernac - -let pr_vernac = make_pr_vernac Ppconstrnew.pr_constr Ppconstrnew.pr_lconstr - -let pr_vernac = function - | VernacRequire (_,_,[Ident(_,r)]) when - (* Obsolete modules *) - List.mem (string_of_id r) - ["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; - "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"; - "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax"; - "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"; - "Zsyntax"] -> - warning ("Forgetting obsolete module "^(string_of_id r)); - mt() - | VernacRequire (exp,spe,[Ident(_,r)]) when - (* Renamed modules *) - List.mem (string_of_id r) ["zarith_aux";"fast_integer"] -> - warning ("Replacing obsolete module "^(string_of_id r)^" with ZArith"); - (str "Require" ++ spc() ++ pr_require_token exp ++ - (match spe with - | None -> mt() - | Some flag -> - (if flag then str"Specification" else str"Implementation") ++ - spc ()) ++ - str "ZArith.") - | VernacImport (false,[Libnames.Ident (_,a)]) when - (* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *) - let a = Names.string_of_id a in - a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt() - | VernacPrint PrintLocalContext -> - warning ("\"Print.\" is discontinued"); - mt () - | x -> pr_vernac x ++ sep_end () - diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli deleted file mode 100644 index e76f1b579b..0000000000 --- a/translate/ppvernacnew.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Pp -open Genarg -open Vernacexpr -open Names -open Nameops -open Nametab -open Util -open Ppconstr -open Pptactic -open Rawterm -open Pcoq -open Libnames -open Ppextend -open Topconstr - -val sep_end : unit -> std_ppcmds - -val pr_vernac : vernac_expr -> std_ppcmds - -val pr_vernac_solve : - int * Environ.env * Tacexpr.glob_tactic_expr * bool -> std_ppcmds |