diff options
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 958 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 100 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 903 | ||||
| -rw-r--r-- | translate/pptacticnew.mli | 28 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 1123 | ||||
| -rw-r--r-- | translate/ppvernacnew.mli | 34 |
6 files changed, 3146 insertions, 0 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml new file mode 100644 index 00000000..7d2feaf2 --- /dev/null +++ b/translate/ppconstrnew.ml @@ -0,0 +1,958 @@ +(************************************************************************) +(* 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: ppconstrnew.ml,v 1.62.2.2 2004/07/16 20:48:17 herbelin Exp $ *) + +(*i*) +open Ast +open Util +open Pp +open Nametab +open Names +open Nameops +open Libnames +open Coqast +open Ppextend +open Topconstr +open Term +open Pattern +(*i*) + +let pr_id id = Nameops.pr_id (Constrextern.v7_to_v8_id id) + +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 Symbols + +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 u = str "<univ>" + +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_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 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 + | CPatNotation (_,"( _ )",[p]) -> + pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom + | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env + | CPatNumeral (_,i) -> Bignat.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 s = string_of_qualid (Constrextern.shortest_qualid_of_v7_global vars ref) in + (str s) + +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 id bl annot t c = + 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 ltop) c + +let pr_fixdecl pr (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 id bl annot t c + +let pr_cofixdecl pr (id,bl,t,c) = + pr_recursive_decl pr id bl (mt()) t c + +let pr_recursive pr_decl id = function + | [] -> anomaly "(co)fixpoint with no definition" + | [d1] -> pr_decl d1 + | dl -> + prlist_with_sep (fun () -> fnl() ++ str "with ") pr_decl 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) -> + let p = hov 0 (str"fix " ++ + pr_recursive (pr_fixdecl (pr mt)) (snd id) fix) in + if List.length fix = 1 & prec_less (fst inherited) ltop + then surround p, latom else p, lfix + | CCoFix (_,id,cofix) -> + let p = + hov 0 (str "cofix " ++ + pr_recursive (pr_cofixdecl (pr mt)) (snd id) cofix) in + if List.length cofix = 1 & prec_less (fst inherited) ltop + then surround p, latom else p, 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 (_,(po,rtntypopt),c,eqns) -> + v 0 + (hv 0 (str "match" ++ brk (1,2) ++ + hov 0 ( + prlist_with_sep sep_v (pr_case_item (pr mt)) c + ++ pr_case_type (pr 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 + + | COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle -> + (* 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_return_type (pr mt) 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 + | COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle -> + hv 0 ( + str "let " ++ + hov 0 (str "(" ++ + prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++ + str ")" ++ + pr_return_type (pr mt) po ++ str " :=" ++ + pr spc ltop c ++ str " in") ++ + pr spc ltop b), + lletin + + | COrderedCase (_,style,po,c,bl) -> + hv 0 ( + str (if style=MatchStyle then "old_match " else "match ") ++ + pr mt ltop c ++ + pr_return_type (pr mt) po ++ + str " with" ++ brk (1,0) ++ + hov 0 (prlist + (fun b -> str "| ??? =>" ++ pr spc ltop b ++ fnl ()) bl) ++ + str "end"), + latom + | 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 (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint + | CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, 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) + +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 transf istype env iscast bl c = + let c' = + if istype then prod_constr_expr c bl + else abstract_constr_expr c bl in + if Options.do_translate() then + let r = + Constrintern.for_grammar + (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[])) + c' in + begin try + (* Try to infer old case and type annotations *) + let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in + (*msgerrnl (str "Typage OK");*) () + with e -> (*msgerrnl (str "Warning: can't type")*) () end; + let c = + (if istype then Constrextern.extern_rawtype + else Constrextern.extern_rawconstr) + (Termops.vars_of_env env) r in + let n = local_binders_length bl in + strip_context n iscast c + else bl, c + +let pr_constr_env env c = pr lsimple (snd (transf false env false [] c)) +let pr_lconstr_env env c = pr ltop (snd (transf false env false [] 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 is_Eval_key c = + Options.do_translate () & + (let f id = let s = string_of_id id in s = "Eval" in + let g = function + | Ident(_,id) -> f id + | Qualid (_,qid) -> let d,id = repr_qualid qid in d = empty_dirpath & f id + in + match c with + | CRef ref | CApp (_,(_,CRef ref),_) when g ref -> true + | _ -> false) + +let pr_protect_eval c = + if is_Eval_key c then h 0 (str "(" ++ pr ltop c ++ str ")") else pr ltop c + +let pr_lconstr_env_n env iscast bl c = + let bl, c = transf false env iscast bl c in + bl, pr_protect_eval c +let pr_type_env_n env bl c = pr ltop (snd (transf true env false bl c)) +let pr_type c = pr ltop (snd (transf true (Global.env()) false [] c)) + +let transf_pattern env c = + if Options.do_translate() then + Constrextern.extern_rawconstr (Termops.vars_of_env env) + (Constrintern.for_grammar + (Constrintern.interp_rawconstr_gen false Evd.empty env true ([],[])) + 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,c) -> + hov 1 (str s ++ pr_arg pr_constr c) + +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 + +let pr_rawconstr_env_no_translate env c = + pr lsimple (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) +let pr_lrawconstr_env_no_translate env c = + pr ltop (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) + +(* 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) + + +(************************************************************************) +(* Automatic standardisation of names in Arith and ZArith by translator *) +(* Very not robust *) + +let is_to_rename dir id = + let dirs = List.map string_of_id (repr_dirpath dir) in + match List.rev dirs with + | "Coq"::"Arith"::"Between"::_ -> false + | "Coq"::"ZArith":: + ("Wf_Z"|"Zpower"|"Zlogarithm"|"Zbinary"|"Zdiv"|"Znumtheory")::_ -> false + | "Coq"::("Arith"|"NArith"|"ZArith")::_ -> true + | "Coq"::"Init"::"Peano"::_ -> true + | "Coq"::"Init"::"Logic"::_ when string_of_id id = "iff_trans" -> true + | "Coq"::"Reals"::"RIneq"::_ -> true + | _ -> false + +let is_ref_to_rename ref = + let sp = sp_of_global ref in + is_to_rename (dirpath sp) (basename sp) + +let get_name (ln,lp,lz,ll,lr,lr') id refbase n = + let id' = string_of_id n in + (match id' with + | "nat" -> (id_of_string (List.hd ln),(List.tl ln,lp,lz,ll,lr,lr')) + | "positive" -> (id_of_string (List.hd lp),(ln,List.tl lp,lz,ll,lr,lr')) + | "Z" -> (id_of_string (List.hd lz),(ln,lp,List.tl lz,ll,lr,lr')) + | "Prop" when List.mem (string_of_id id) ["a";"b";"c"] -> + (* pour iff_trans *) + (id_of_string (List.hd ll),(ln,lp,lz,List.tl ll,lr,lr')) + | "R" when (* Noms r,r1,r2 *) + refbase = "Rle_refl" or + refbase = "Rlt_monotony_contra" or + refbase = "Rmult_le_reg_l" or + refbase = "Rle_monotony_contra" or + refbase = "Rge_monotony" -> + (id_of_string (List.hd lr')),(ln,lp,lz,ll,lr,List.tl lr') + | "R" when (* Noms r1,r2,r3,r4 *) + List.mem (string_of_id id) + ["x";"y";"x'";"y'";"z";"t";"n";"m";"a";"b";"c";"p";"q"] + & refbase <> "sum_inequa_Rle_lt" + -> + (id_of_string (List.hd lr),(ln,lp,lz,ll,List.tl lr,lr')) + | _ -> id,(ln,lp,lz,ll,lr,lr')) + +let get_name_constr names id refbase t = match kind_of_term t with + | Ind ind -> + let n = basename (sp_of_global (IndRef ind)) in + get_name names id refbase n + | Const sp -> + let n = basename (sp_of_global (ConstRef sp)) in + get_name names id refbase n + | Sort _ -> get_name names id refbase (id_of_string "Prop") + | _ -> id,names + +let names = + (["n";"m";"p";"q"],["p";"q";"r";"s"],["n";"m";"p";"q"],["A";"B";"C"], + ["r1";"r2";"r3";"r4"],["r";"r1";"r2"]) + +let znames refbase t = + let rec aux c names = match kind_of_term c with + | Prod (Name id as na,t,c) -> + let (id,names) = get_name_constr names id refbase t in + (na,id) :: aux c names + | Prod (Anonymous,t,c) -> + (Anonymous,id_of_string "ZZ") :: aux c names + | _ -> [] + in aux t names + +let get_name_raw names id refbase t = match t with + | CRef(Ident (_,n)) -> get_name names id refbase n + | CSort _ -> get_name names id refbase (id_of_string "Prop") + | _ -> id,names + +let rename_bound_variables id0 t = + if is_to_rename (Lib.library_dp()) id0 then + let refbase = string_of_id id0 in + let rec aux c names subst = match c with + | CProdN (loc,bl,c) -> + let rec aux2 names subst = function + | (nal,t)::bl -> + let rec aux3 names subst = function + | (loc,Name id)::nal -> + let (id',names) = get_name_raw names id refbase t in + let (nal,names,subst) = aux3 names ((id,id')::subst) nal in + (loc,Name id')::nal, names, subst + | x::nal -> + let (nal,names,subst) = aux3 names subst nal in + x::nal,names,subst + | [] -> [],names,subst in + let t = replace_vars_constr_expr subst t in + let nal,names,subst = aux3 names subst nal in + let bl,names,subst = aux2 names subst bl in + (nal,t)::bl, names, subst + | [] -> [],names,subst in + let bl,names,subst = aux2 names subst bl in + CProdN (loc,bl,aux c names subst) + | CArrow (loc,t,u) -> + let u = aux u names subst in + CArrow (loc,replace_vars_constr_expr subst t,u) + | _ -> replace_vars_constr_expr subst c + in aux t names [] + else t + +let translate_binding kn n ebl = + let t = Retyping.get_type_of (Global.env()) Evd.empty (mkConst kn) in + let subst= znames (string_of_id (basename (sp_of_global (ConstRef kn)))) t in + try + let _,subst' = list_chop n subst in + List.map (function + | (x,NamedHyp id,c) -> (x,NamedHyp (List.assoc (Name id) subst'),c) + | x -> x) ebl + with _ -> ebl + +let translate_with_bindings c bl = + match bl with + | ExplicitBindings l -> + let l = match c with + | RRef (_,(ConstRef kn as ref)) when is_ref_to_rename ref -> + translate_binding kn 0 l + | RApp (_,RRef (_,(ConstRef kn as ref)),args) when is_ref_to_rename ref + -> translate_binding kn (List.length args) l + | _ -> + l + in ExplicitBindings l + | x -> x diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli new file mode 100644 index 00000000..4477728c --- /dev/null +++ b/translate/ppconstrnew.mli @@ -0,0 +1,100 @@ +(************************************************************************) +(* 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: ppconstrnew.mli,v 1.16.2.1 2004/07/16 19:31:52 herbelin Exp $ *) + +open Pp +open Environ +open Term +open Libnames +open Pcoq +open Rawterm +open Extend +open Coqast +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_lconstr_env_n : env -> bool -> local_binder list -> constr_expr -> + local_binder list * std_ppcmds +val pr_type_env_n : env -> local_binder list -> 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_rawconstr_env_no_translate : env -> rawconstr -> std_ppcmds +val pr_lrawconstr_env_no_translate : 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 + +(* To translate names in ZArith *) +val translate_with_bindings : rawconstr -> 'a bindings -> 'a bindings +val rename_bound_variables : identifier -> constr_expr -> constr_expr diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml new file mode 100644 index 00000000..80298c3e --- /dev/null +++ b/translate/pptacticnew.ml @@ -0,0 +1,903 @@ +(************************************************************************) +(* 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: pptacticnew.ml,v 1.57.2.2 2004/07/16 19:31:52 herbelin Exp $ *) + +open Pp +open Names +open Nameops +open Environ +open Util +open Extend +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 v8 syntax only double quote char is escaped by repeating it *) +let rec escape_string_v8 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 qstringnew s = str ("\""^escape_string_v8 s^"\"") +let qsnew = qstringnew + +let translate_v7_ltac = function + | "DiscrR" -> "discrR" + | "Sup0" -> "prove_sup0" + | "SupOmega" -> "omega_sup" + | "Sup" -> "prove_sup" + | "RCompute" -> "Rcompute" + | "IntroHypG" -> "intro_hyp_glob" + | "IntroHypL" -> "intro_hyp_pt" + | "IsDiff_pt" -> "is_diff_pt" + | "IsDiff_glob" -> "is_diff_glob" + | "IsCont_pt" -> "is_cont_pt" + | "IsCont_glob" -> "is_cont_glob" + | "RewTerm" -> "rew_term" + | "ConsProof" -> "deriv_proof" + | "SimplifyDerive" -> "simplify_derive" + | "Reg" -> "reg" (* ??? *) + | "SplitAbs" -> "split_case_Rabs" + | "SplitAbsolu" -> "split_Rabs" + | "SplitRmult" -> "split_Rmult" + | "CaseEqk" -> "case_eq" + | "SqRing" -> "ring_Rsqr" + | "TailSimpl" -> "tail_simpl" + | "CoInduction" -> "coinduction" + | "ElimCompare" -> "elim_compare" + | "CCsolve" -> "CCsolve" (* ?? *) + | "ArrayAccess" -> "array_access" + | "MemAssoc" -> "mem_assoc" + | "SeekVarAux" -> "seek_var_aux" + | "SeekVar" -> "seek_var" + | "NumberAux" -> "number_aux" + | "Number" -> "number" + | "BuildVarList" -> "build_varlist" + | "Assoc" -> "assoc" + | "Remove" -> "remove" + | "Union" -> "union" + | "RawGiveMult" -> "raw_give_mult" + | "GiveMult" -> "give_mult" + | "ApplyAssoc" -> "apply_assoc" + | "ApplyDistrib" -> "apply_distrib" + | "GrepMult" -> "grep_mult" + | "WeakReduce" -> "weak_reduce" + | "Multiply" -> "multiply" + | "ApplyMultiply" -> "apply_multiply" + | "ApplyInverse" -> "apply_inverse" + | "StrongFail" -> "strong_fail" + | "InverseTestAux" -> "inverse_test_aux" + | "InverseTest" -> "inverse_test" + | "ApplySimplif" -> "apply_simplif" + | "Unfolds" -> "unfolds" + | "Reduce" -> "reduce" + | "Field_Gen_Aux" -> "field_gen_aux" + | "Field_Gen" -> "field_gen" + | "EvalWeakReduce" -> "eval_weak_reduce" + | "Field_Term" -> "field_term" + | "Fourier" -> "fourier" (* ou Fourier ?? *) + | "FourierEq" -> "fourier_eq" + | "S_to_plus" -> "rewrite_S_to_plus_term" + | "S_to_plus_eq" -> "rewrite_S_to_plus" + | "NatRing" -> "ring_nat" + | "Solve1" -> "solve1" + | "Solve2" -> "solve2" + | "Elim_eq_term" -> "elim_eq_term" + | "Elim_eq_Z" -> "elim_eq_Z" + | "Elim_eq_pos" -> "elim_eq_pos" + | "Elim_Zcompare" -> "elim_Zcompare" + | "ProveStable" -> "prove_stable" + | "interp_A" -> "interp_A" + | "InitExp" -> "init_exp" + | "SimplInv" -> "simpl_inv" + | "Map" -> "map_tactic" + | "BuildMonomAux" -> "build_monom_aux" + | "BuildMonom" -> "build_monom" + | "SimplMonomAux" -> "simpl_monom_aux" + | "SimplMonom" -> "simpl_monom" + | "SimplAllMonoms" -> "simpl_all_monomials" + | "AssocDistrib" -> "assoc_distrib" + | "NowShow" -> "now_show" + | ("subst"|"simpl"|"elim"|"destruct"|"apply"|"intro" (* ... *)) as x -> + let x' = x^"_" in + msgerrnl + (str ("Warning: '"^ + x^"' is now a primitive tactic; it has been translated to '"^x'^"'")); + x' + | x -> x + +let id_of_ltac_v7_id id = + id_of_string (translate_v7_ltac (string_of_id id)) + +let pr_ltac_or_var pr = function + | ArgArg x -> pr x + | ArgVar (loc,id) -> + pr_with_comments loc (pr_id (id_of_ltac_v7_id id)) + +let pr_arg pr x = spc () ++ pr x + +let pr_ltac_constant sp = + (* Source de bug: le nom le plus court n'est pas forcement correct + apres renommage *) + let qid = Nametab.shortest_qualid_of_tactic sp in + let dir,id = repr_qualid qid in + pr_qualid (make_qualid dir (id_of_ltac_v7_id id)) + +let pr_evaluable_reference_env env = function + | EvalVarRef id -> pr_id (Constrextern.v7_to_v8_id id) + | EvalConstRef sp -> pr_global (Termops.vars_of_env env) (Libnames.ConstRef sp) + +let pr_inductive vars ind = pr_global vars (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_binding prc = function + | NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) + | AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) +*) + +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) = + if Options.do_translate () then + (* translator calls pr_with_bindings on rawconstr: we cast it! *) + let bl' = translate_with_bindings (fst (Obj.magic c) : rawconstr) bl in + hov 1 (prc c ++ pr_bindings prlc prc bl') + else + 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_hyp_location pr_id (id,occs,(hl,hl')) = + if !hl' <> None then pr_hyp_location pr_id (id,occs,out_some !hl') + else + (if hl = InHyp && Options.do_translate () then + msgerrnl (h 0 (str "Translator warning: Unable to detect if " ++ pr_id id ++ spc () ++ str "denotes a local definition")); + pr_hyp_location pr_id (id,occs,hl)) + +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_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_as_names_force force ids (pp,ids') = + pr_with_names + (if (!pp or force) & List.exists ((<>) (ref [])) ids' + then Some (IntroOrAndPattern (List.map (fun x -> !x) ids')) + else ids) + +let duplicate force nodup ids pr = function + | [] -> pr (pr_as_names_force force ids (ref false,[])) + | x::l when List.for_all (fun y -> snd x=snd y) l -> + pr (pr_as_names_force force ids x) + | l -> + if List.exists (fun (b,ids) -> !b) l & (force or + List.exists (fun (_,ids) -> ids <> (snd (List.hd l))) (List.tl l)) + then + if nodup then begin + msgerrnl + (h 0 (str "Translator warning: Unable to enforce v7 names while translating Induction/NewDestruct/NewInduction. Names in the different branches are") ++ brk (0,0) ++ + hov 0 (prlist_with_sep spc + (fun id -> hov 0 (pr_as_names_force true ids id)) + (List.rev l))); + pr (pr_as_names_force force ids (ref false,[])) + end + else + pr_seq_body (fun x -> pr (pr_as_names_force force ids x)) (List.rev l) + else pr (pr_as_names_force force ids (ref false,[])) + +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 ";" + + +open Closure + +let make_pr_tac (pr_tac,pr_tac0,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_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" +(* | TacAutoTDB None -> str "autotdb" + | TacDestructConcl -> str "dconcl"*) + | 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 (pr_constr env) (pr_lconstr env) (pr_tac env) s l) + | TacAlias (loc,s,l,_) -> + pr_with_comments loc + (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) 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) + | 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) -> + if Options.do_translate () then + (* Pose was buggy and was wrongly substituted in conclusion in v7 *) + hov 1 (str "set" ++ pr_constrarg env c) + else + hov 1 (str "pose" ++ pr_constrarg env c) + | TacForward (true,Name id,c) -> + if Options.do_translate () then + hov 1 (str "set" ++ spc() ++ + hov 1 (str"(" ++ pr_id id ++ str " :=" ++ + pr_lconstrarg env c ++ str")")) + else + 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,cls) -> + hov 1 (str "instantiate" ++ spc() ++ + hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ + pr_lconstrarg env c ++ str ")" ++ + pr_clauses pr_ident cls)) + (* Derived basic tactics *) + | TacSimpleInduction (h,l) -> + if List.exists (fun (pp,_) -> !pp) !l then + duplicate true true None (fun pnames -> + hov 1 (str "induction" ++ pr_arg pr_quantified_hypothesis h ++ + pnames)) !l + else + hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) + | TacNewInduction (h,e,(ids,l)) -> + duplicate false true ids (fun pnames -> + hov 1 (str "induction" ++ spc () ++ + pr_induction_arg (pr_constr env) h ++ pnames ++ + pr_opt (pr_eliminator env) e)) !l + | TacSimpleDestruct h -> + hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) + | TacNewDestruct (h,e,(ids,l)) -> + duplicate false true ids (fun pnames -> + hov 1 (str "destruct" ++ spc () ++ + pr_induction_arg (pr_constr env) h ++ pnames ++ + pr_opt (pr_eliminator env) e)) !l + | 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) -> + let vars = Termops.vars_of_env env in + hov 1 (str "decompose" ++ spc () ++ + hov 0 (str "[" ++ prlist_with_sep spc (pr_ind vars) 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 int n ++ pr_hintbases db) +(* | TacAutoTDB None as x -> pr_atom0 env x + | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n) + | TacDestructHyp (true,id) -> + hov 0 (str "cdhyp" ++ spc () ++ pr_lident id) + | TacDestructHyp (false,id) -> + hov 0 (str "dhyp" ++ spc () ++ pr_lident id) + | TacDestructConcl as x -> pr_atom0 env x + | TacSuperAuto (n,l,b1,b2) -> + hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ + pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)*) + | TacDAuto (n,p) -> + hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p) + + (* Context management *) + | TacClear l -> + hov 1 (str "clear" ++ spc () ++ 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_tac0 env) 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 (pr_constr env,pr_lconstr env,pr_cst 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 ltop = (5,E) in +let lseq = 5 in +let ltactical = 3 in +let lorelse = 2 in +let llet = 1 in +let lfun = 1 in +let labstract = 3 in +let lmatch = 1 in +let latom = 0 in +let lcall = 1 in +let leval = 1 in +let ltatom = 1 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 (t,lrul) -> + hov 0 (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 (lr,lrul) -> + hov 0 ( + 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) -> + 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) -> + let pp2 = + (* Hook for translation names in induction/destruct *) + match t2 with + | TacAtom (_,TacSimpleInduction (h,l)) -> + if List.exists (fun (pp,ids) -> !pp) !l then + duplicate true false None (fun pnames -> + hov 1 + (str "induction" ++ pr_arg pr_quantified_hypothesis h ++ + pnames)) !l + else + hov 1 + (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) + | TacAtom (_,TacNewInduction (h,e,(ids,l))) -> + duplicate false false ids (fun pnames -> + hov 1 (str "induction" ++ spc () ++ + pr_induction_arg (pr_constr env) h ++ pnames ++ + pr_opt (pr_eliminator env) e)) !l + | TacAtom (_,TacNewDestruct (h,e,(ids,l))) -> + duplicate false false ids (fun pnames -> + hov 1 (str "destruct" ++ spc () ++ + pr_induction_arg (pr_constr env) h ++ pnames ++ + pr_opt (pr_eliminator env) e)) !l + (* end hook *) + | _ -> pr_tac env (lseq,L) t2 in + hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++ pp2), + 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 qsnew 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" ++ (qsnew s), latom + | TacAtom (loc,t) -> + pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom + | TacArg(Tacexp e) -> pr_tac0 env 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 qsnew 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 qsnew sopt + | (TacCall _|Tacexp _|Integer _) as a -> + str "ltac:" ++ pr_tac env (latom,E) (TacArg a) + +in ((fun env -> pr_tac env ltop), + (fun env -> pr_tac env (latom,E)), + pr_match_rule) + +let pi1 (a,_,_) = a +let pi2 (_,a,_) = a +let pi3 (_,_,a) = a + +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 rec raw_printers = + (pr_raw_tactic, + pr_raw_tactic0, + Ppconstrnew.pr_constr_env, + Ppconstrnew.pr_lconstr_env, + Ppconstrnew.pr_pattern, + (fun _ -> pr_reference), + (fun _ -> pr_reference), + pr_reference, + pr_or_metaid pr_lident, + Pptactic.pr_raw_extend, + strip_prod_binders_expr) + +and pr_raw_tactic env (t:raw_tactic_expr) = + pi1 (make_pr_tac raw_printers) env t + +and pr_raw_tactic0 env t = + pi2 (make_pr_tac raw_printers) env t + +and pr_raw_match_rule env t = + pi3 (make_pr_tac raw_printers) env t + +let pr_and_constr_expr pr (c,_) = pr c + + +let rec glob_printers = + (pr_glob_tactic, + pr_glob_tactic0, + (fun env -> pr_and_constr_expr (Ppconstrnew.pr_rawconstr_env_no_translate env)), + (fun env -> pr_and_constr_expr (Ppconstrnew.pr_lrawconstr_env_no_translate 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 vars -> pr_or_var (pr_inductive vars)), + pr_ltac_or_var (pr_located pr_ltac_constant), + pr_lident, + Pptactic.pr_glob_extend, + strip_prod_binders_rawterm) + +and pr_glob_tactic env (t:glob_tactic_expr) = + pi1 (make_pr_tac glob_printers) env t + +and pr_glob_tactic0 env t = + pi2 (make_pr_tac glob_printers) env t + +and pr_glob_match_rule env t = + pi3 (make_pr_tac glob_printers) env t + +let (pr_tactic,_,_) = + make_pr_tac + (pr_glob_tactic, + pr_glob_tactic0, + 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) + diff --git a/translate/pptacticnew.mli b/translate/pptacticnew.mli new file mode 100644 index 00000000..2558413f --- /dev/null +++ b/translate/pptacticnew.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* 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: pptacticnew.mli,v 1.6.2.1 2004/07/16 19:31:52 herbelin Exp $ *) + +open Pp +open Genarg +open Tacexpr +open Proof_type +open Topconstr +open Names + +val qsnew : string -> std_ppcmds + +val pr_raw_tactic : Environ.env -> raw_tactic_expr -> std_ppcmds + +val pr_glob_tactic : Environ.env -> glob_tactic_expr -> std_ppcmds + +val pr_tactic : Environ.env -> Proof_type.tactic_expr -> std_ppcmds + +val id_of_ltac_v7_id : identifier -> identifier + + diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml new file mode 100644 index 00000000..246253eb --- /dev/null +++ b/translate/ppvernacnew.ml @@ -0,0 +1,1123 @@ +(************************************************************************) +(* 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: ppvernacnew.ml,v 1.95.2.2 2004/07/16 20:48:17 herbelin Exp $ *) + +open Pp +open Names +open Nameops +open Nametab +open Util +open Extend +open Vernacexpr +open Ppconstrnew +open Pptacticnew +open Rawterm +open Coqast +open Genarg +open Pcoq +open Ast +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 pr_lname = function + (loc,Name id) -> pr_lident (loc,id) + | lna -> pr_located pr_name lna + +let pr_ltac_id id = Nameops.pr_id (id_of_ltac_v7_id 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 + 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_env env) + (Ppconstrnew.pr_lconstr_env env) + (Pptacticnew.pr_raw_tactic env) pr_reference t + +let pr_raw_tactic tac = + pr_raw_tactic_env [] (Global.env()) 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 + | (s,pargs)::rls -> + if extract_signature pargs = tys then (s,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 pr_non_terminal = function + | NtQual (u,nt) -> (* no more qualified entries *) str nt + | NtShort "constrarg" -> str "constr" + | NtShort nt -> str nt + +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) -> pr_non_terminal nt ++ str"(" ++ pr_id (strip_meta p) ++ str")" + | VNonTerm (loc,nt,None) -> pr_non_terminal 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 pr_aux = function + | CAppExpl (_,(_,qid),[]) -> pr_reference qid + | _ -> mt () 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_lident id ++ str" := " ++ p + | CWith_Module (id,qid) -> + str"Module" ++ spc() ++ pr_lident 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_module_vardecls pr_c (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"(" ++ 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_opt_casted_constr pr_c = function + | CCast (loc,c,t) -> pr_c c ++ str":" ++ pr_c t + | _ as c -> pr_c c +*) + +let pr_type_option pr_c = function + | CHole loc -> mt() + | _ as c -> brk(0,2) ++ str":" ++ pr_c c + +let without_translation f x = + let old = Options.do_translate () in + let oldv7 = !Options.v7 in + Options.make_translate false; + try let r = f x in Options.make_translate old; Options.v7:=oldv7; r + with e -> Options.make_translate old; Options.v7:=oldv7; raise e + +let pr_decl_notation prc = + pr_opt (fun (ntn,c,scopt) -> fnl () ++ + str "where " ++ qsnew ntn ++ str " := " ++ without_translation 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 = + let bl, _ = pr_lconstr_env_n (Global.env()) false bl (CHole dummy_loc) in + 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_require_token = function + | Some true -> str " Export" + | Some false -> str " Import" + | None -> mt() + +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 pr_grammar_tactic_rule (name,(s,pil),t) = +(* + hov 0 ( + (* str name ++ spc() ++ *) + hov 0 (str"[" ++ qsnew s ++ spc() ++ + prlist_with_sep sep pr_production_item pil ++ str"]") ++ + spc() ++ hov 0 (str"->" ++ spc() ++ str"[" ++ pr_raw_tactic t ++ str"]")) +*) + hov 2 (str "Tactic Notation" ++ spc() ++ + hov 0 (qsnew s ++ spc() ++ 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 + | 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") + | 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 + + (* 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 *) + | VernacGrammar _ -> + msgerrnl (str"Warning : constr Grammar is discontinued; use Notation"); + str"(* <Warning> : Grammar is replaced by Notation *)" + | VernacTacticGrammar l -> + prlist_with_sep (fun () -> sep_end() ++ fnl()) pr_grammar_tactic_rule l +(* + hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***) +*) + | VernacSyntax (u,el) -> + msgerrnl (str"Warning : Syntax is discontinued; use Notation"); + str"(* <Warning> : Syntax is discontinued" ++ +(* + fnl () ++ + hov 1 (str"Syntax " ++ str u ++ spc() ++ + prlist_with_sep sep_v2 pr_syntax_entry el) ++ +*) + str " *)" + | 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,_),q,ov8,sn) -> (* A Verifier *) + let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in + hov 0 (hov 0 (str"Infix " ++ pr_locality local + ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++ + pr_syntax_modifiers mv8 ++ + (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + | VernacDistfix (local,a,p,s,q,sn) -> + hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p + ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with + | None -> mt() + | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) + | VernacNotation (local,c,sl,mv8,opt) -> + let (s,l) = match mv8 with + None -> fst (out_some sl), [] + | Some ml -> ml in + 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,sl,mv8) -> + let (s,l) = match mv8 with + None -> out_some sl + | Some ml -> ml in + 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 -> 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 mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in + let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in + let pr_def_body = function + | DefineBody (bl,red,c,d) -> + let (bl2,body,ty) = match d with + | None -> + let bl2,body = extract_lam_binders c in + (bl2,body,mt()) + | Some ty -> + let bl2,body,ty' = extract_def_binders c ty in + (bl2,CCast (dummy_loc,body,ty'), + spc() ++ str":" ++ + pr_sep_com spc + (pr_type_env_n (Global.env()) (bl@bl2)) ty') in + let iscast = d <> None in + let bindings,ppred = + pr_lconstr_env_n (Global.env()) iscast (bl@bl2) body in + (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred)) + | ProveBody (bl,t) -> + (pr_and_type_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() + | _ -> error "Statements with local binders no longer supported") + ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) 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) -> + hov 2 + (pr_assumption_token (List.length l > 1) stre ++ spc() ++ + pr_ne_params_list pr_type l) + | VernacInductive (f,l) -> + + (* Copie simplifiée de command.ml pour recalculer les implicites, *) + (* les notations, et le contexte d'evaluation *) + let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in + let nparams = local_binders_length lparams + and sigma = Evd.empty + and env0 = Global.env() in + let (env_params,params) = + List.fold_left + (fun (env,params) d -> match d with + | LocalRawAssum (nal,t) -> + let t = Constrintern.interp_type sigma env t in + let ctx = list_map_i (fun i (_,na) -> (na,None,Term.lift i t)) 0 nal + in let ctx = List.rev ctx in + (Environ.push_rel_context ctx env, ctx@params) + | LocalRawDef ((_,na),c) -> + let c = Constrintern.judgment_of_rawconstr sigma env c in + let d = (na, Some c.Environ.uj_val, c.Environ.uj_type) in + (Environ.push_rel d env,d::params)) + (env0,[]) lparams in + + let (ind_env,ind_impls,arityl) = + List.fold_left + (fun (env, ind_impls, arl) ((_,recname), _, _, arityc, _) -> + let arity = Constrintern.interp_type sigma env_params arityc in + let fullarity = Termops.it_mkProd_or_LetIn arity params in + let env' = Termops.push_rel_assum (Name recname,fullarity) env in + let impls = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env_params fullarity + else [] in + (env', (recname,impls)::ind_impls, (arity::arl))) + (env0, [], []) l + in + let lparnames = List.map (fun (na,_,_) -> na) params in + let notations = + List.fold_right (fun (_,ntnopt,_,_,_) l ->option_cons ntnopt l) l [] in + let ind_env_params = Environ.push_rel_context params ind_env in + + let lparnames = List.map (fun (na,_,_) -> na) params in + let impl = List.map + (fun ((_,recname),_,_,arityc,_) -> + let arity = Constrintern.interp_type sigma env_params arityc in + let fullarity = + Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params) + in + let impl_in = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env_params fullarity + else [] in + let impl_out = + if Impargs.is_implicit_args_out() + then Impargs.compute_implicits true env_params fullarity + else [] in + (recname,impl_in,impl_out)) l in + let impls_in = List.map (fun (id,a,_) -> (id,a)) impl in + let impls_out = List.map (fun (id,_,a) -> (id,a)) impl in + Constrintern.set_temporary_implicits_in impls_in; + Constrextern.set_temporary_implicits_out impls_out; + (* Fin calcul implicites *) + + let pr_constructor (coe,(id,c)) = + hov 2 (pr_lident id ++ str" " ++ + (if coe then str":>" else str":") ++ + pr_sep_com spc (pr_type_env_n ind_env_params []) 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 + + (* Copie simplifiée de command.ml pour déclarer les notations locales *) + List.iter (fun (df,c,scope) -> + Metasyntax.add_notation_interpretation df [] c scope) notations; + + 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 -> + + (* Copie simplifiée de command.ml pour recalculer les implicites *) + (* les notations, et le contexte d'evaluation *) + let sigma = Evd.empty + and env0 = Global.env() in + let notations = + List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in + let impl = List.map + (fun ((recname,_, bl, arityc,_),_) -> + let arity = + Constrintern.interp_type sigma env0 + (prod_constr_expr arityc bl) in + let impl_in = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env0 arity + else [] in + let impl_out = + if Impargs.is_implicit_args_out() + then Impargs.compute_implicits true env0 arity + else [] in + (recname,impl_in,impl_out)) recs in + let impls_in = List.map (fun (id,a,_) -> (id,a)) impl in + let impls_out = List.map (fun (id,_,a) -> (id,a)) impl in + Constrintern.set_temporary_implicits_in impls_in; + Constrextern.set_temporary_implicits_out impls_out; + + (* Copie simplifiée de command.ml pour déclarer les notations locales *) + List.iter (fun (df,c,scope) -> + Metasyntax.add_notation_interpretation df [] c None) notations; + + let rec_sign = + List.fold_left + (fun env ((recname,_,bl,arityc,_),_) -> + let arity = + Constrintern.interp_type sigma env0 + (prod_constr_expr arityc bl) in + Environ.push_named (recname,None,arity) env) + (Global.env()) recs in + + 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 + let bl,ppc = + pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in + pr_id id ++ pr_binders_arg bl ++ annot ++ spc() + ++ pr_type_option (fun c -> spc() ++ pr_type c) type_ + ++ str" :=" ++ brk(1,1) ++ ppc ++ + pr_decl_notation pr_constr ntn + in + hov 1 (str"Fixpoint" ++ spc() ++ + prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs) + + | VernacCoFixpoint corecs -> + 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 + hov 1 (str"CoFixpoint" ++ 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" ++ pr_require_token exp ++ spc() ++ + (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 (m,bl,ty,bd) -> + let b = pr_module_binders_list bl pr_lconstr in + hov 2 (str"Module " ++ pr_lident m ++ b ++ + pr_opt (pr_of_module_type pr_lconstr) ty ++ + pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) + | VernacDeclareModule (id,bl,m1,m2) -> + let b = pr_module_binders_list bl pr_lconstr in + hov 2 (str"Declare Module " ++ pr_lident id ++ b ++ + pr_opt (pr_of_module_type pr_lconstr) m1 ++ + pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2) + | 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 " ++ pr_require_token exp ++ spc() ++ + (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" + | PrintCoercions -> str"Print Coercions" + | PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t + | 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 + | 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 + | 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 + | 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 + | VernacV7only _ -> mt() + | VernacV8only com -> pr_vernac com + | 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 + (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *) + let s = + let n = String.length s in + if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "V7" + then String.sub s 0 (n-2) ^ "V8" + else s in + (* "Hint Rewrite in using" changes the order of its args in v8 !! *) + let cl = match s, cl with + | "HintRewriteV8", [a;b;c;d] -> [a;b;d;c] + | _ -> cl in + let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in + let (hd,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)) + (str hd,cl) rl in + hov 1 pp + ++ (if s = "Correctness" then sep_end () ++ fnl() ++ str "Proof" else mt()) + 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" ++ pr_require_token exp ++ spc() ++ + (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() + | VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x + | VernacPrint PrintLocalContext -> + warning ("\"Print.\" is discontinued"); + mt () + | x -> pr_vernac x ++ sep_end () + diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli new file mode 100644 index 00000000..73101a1a --- /dev/null +++ b/translate/ppvernacnew.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* 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: ppvernacnew.mli,v 1.3.2.1 2004/07/16 19:31:52 herbelin Exp $ *) + +open Pp +open Genarg +open Vernacexpr +open Names +open Nameops +open Nametab +open Util +open Extend +open Ppconstr +open Pptactic +open Rawterm +open Coqast +open Pcoq +open Ast +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 |