From e03d1840a8e6eec927e7fbe006d59ab21b8d818f Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Oct 2008 11:21:45 +0000 Subject: Affichage des notations récursives: - Prise en compte des notations applicatives - Remplacement du codage des arguments liste des notations récursives sous forme de terme par une représentation directe (permet notamment de résoudre un problème de stack overflow de la fonction d'affichage) + Correction bug affichage Lemma dans ppvernac.ml + Divers util.ml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11489 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egrammar.ml | 46 +++++++++++++++++++++--------------------- parsing/g_constr.ml4 | 4 ++-- parsing/ppconstr.ml | 56 ++++++++++++++++++++++++---------------------------- parsing/ppvernac.ml | 4 ++-- parsing/q_coqast.ml4 | 6 ++++-- 5 files changed, 56 insertions(+), 60 deletions(-) (limited to 'parsing') diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index bd688bcdd..585d7ab82 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -52,58 +52,56 @@ type prod_item = | NonTerm of constr_production_entry * (Names.identifier * constr_production_entry) option -type 'a action_env = (identifier * 'a) list +type 'a action_env = 'a list * 'a list list let make_constr_action (f : loc -> constr_expr action_env -> constr_expr) pil = - let rec make (env : constr_expr action_env) = function + let rec make (env,envlist as fullenv : constr_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc env) + Gramext.action (fun loc -> f loc fullenv) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gramext.action (fun _ -> make fullenv tl) | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *) - Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl) + Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl) | Some (p, ETReference) :: tl -> (* non-terminal *) - Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl) + Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl) | Some (p, ETIdent) :: tl -> (* non-terminal *) Gramext.action (fun (v:identifier) -> - make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) + make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) Gramext.action (fun (v:Bigint.bigint) -> - make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl) + make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl) | Some (p, ETConstrList _) :: tl -> - Gramext.action (fun (v:constr_expr list) -> - let dummyid = Ident (dummy_loc,id_of_string "_") in - make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl) + Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) | Some (p, ETPattern) :: tl -> failwith "Unexpected entry of type cases pattern" in - make [] (List.rev pil) + make ([],[]) (List.rev pil) let make_cases_pattern_action (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil = - let rec make (env : cases_pattern_expr action_env) = function + let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc env) + Gramext.action (fun loc -> f loc fullenv) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gramext.action (fun _ -> make fullenv tl) | Some (p, ETConstr _) :: tl -> (* pattern non-terminal *) - Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl) + Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) | Some (p, ETReference) :: tl -> (* non-terminal *) Gramext.action (fun (v:reference) -> - make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl) + make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) | Some (p, ETIdent) :: tl -> (* non-terminal *) Gramext.action (fun (v:identifier) -> - make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl) + make + (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) Gramext.action (fun (v:Bigint.bigint) -> - make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl) + make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:cases_pattern_expr list) -> - let dummyid = Ident (dummy_loc,id_of_string "_") in - make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl) + make (env, v :: envlist) tl) | Some (p, (ETPattern | ETOther _)) :: tl -> failwith "Unexpected entry of type cases pattern or other" in - make [] (List.rev pil) + make ([],[]) (List.rev pil) let make_constr_prod_item univ assoc from forpat = function | Term tok -> (Gramext.Stoken tok, None) @@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt = let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) - let mkact loc env = CNotation (loc,ntn,List.map snd env) in + let mkact loc env = CNotation (loc,ntn,env) in let e = get_constr_entry false (ETConstr (n,())) in extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule; (* Add the notation in cases_pattern *) - let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in + let mkact loc env = CPatNotation (loc,ntn,env) in let e = get_constr_entry true (ETConstr (n,())) in extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rule diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b8dcf8e99..740ba0b34 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -202,7 +202,7 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c with CPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CNotation(loc,"( _ )",[c]) + CNotation(loc,"( _ )",([c],[])) | _ -> c) ] ] ; forall: @@ -337,7 +337,7 @@ GEXTEND Gram | "("; p = pattern LEVEL "200"; ")" -> (match p with CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CPatNotation(loc,"( _ )",[p]) + CPatNotation(loc,"( _ )",([p],[])) | _ -> p) | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (loc, String s) ] ] diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 4f266f5ca..e906fb398 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -62,36 +62,32 @@ let prec_of_prim_token = function | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint | String _ -> latom -let env_assoc_value v env = - try List.nth env (v-1) - with Not_found -> anomaly ("Inconsistent environment for pretty-print rule") - -let decode_constrlist_value = function - | CAppExpl (_,_,l) -> l - | CApp (_,_,l) -> List.map fst l - | _ -> anomaly "Ill-formed list argument of notation" - -let decode_patlist_value = function - | CPatCstr (_,_,l) -> l - | _ -> anomaly "Ill-formed list argument of notation" - open Notation -let rec print_hunk n decode pr env = function - | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env) - | UnpListMetaVar (e,prec,sl) -> - prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl) - (pr (n,prec)) (decode (env_assoc_value e env)) - | UnpTerminal s -> str s - | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub) - | UnpCut cut -> ppcmd_of_cut cut - -let pr_notation_gen decode pr s env = +let print_hunks n pr (env,envlist) unp = + let env = ref env and envlist = ref envlist in + let pop r = let a = List.hd !r in r := List.tl !r; a in + let rec aux = function + | [] -> mt () + | UnpMetaVar (_,prec) :: l -> + let c = pop env in pr (n,prec) c ++ aux l + | UnpListMetaVar (_,prec,sl) :: l -> + let cl = pop envlist in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in + let pp2 = aux l in + pp1 ++ pp2 + | UnpTerminal s :: l -> str s ++ aux l + | UnpBox (b,sub) :: l -> + (* Keep order: side-effects *) + let pp1 = ppcmd_of_box b (aux sub) in + let pp2 = aux l in + pp1 ++ pp2 + | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in + aux unp + +let pr_notation 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 + print_hunks level pr env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -179,9 +175,9 @@ let rec pr_patt sep inh p = | CPatAtom (_,Some r) -> pr_reference r, latom | CPatOr (_,pl) -> hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator - | CPatNotation (_,"( _ )",[p]) -> + | CPatNotation (_,"( _ )",([p],[])) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env + | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in @@ -592,7 +588,7 @@ let rec pr sep inherited a = | CCast (_,a,CastCoerce) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), lcast - | CNotation (_,"( _ )",[t]) -> + | CNotation (_,"( _ )",([t],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index f779f53fb..2233bbd6a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -539,11 +539,11 @@ let rec pr_vernac = function | VernacStartTheoremProof (ki,l,_,_) -> let pr_statement head (id,(bl,c)) = hov 0 - (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++ + (head ++ pr_opt pr_lident id ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_lconstr c) in hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ - prlist (pr_statement (str "with ")) (List.tl l)) + prlist (pr_statement (spc () ++ str "with")) (List.tl l)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 37350af08..8407211f1 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -159,9 +159,11 @@ let rec mlexpr_of_constr = function | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >> | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" - | Topconstr.CNotation(_,ntn,l) -> + | Topconstr.CNotation(_,ntn,subst) -> <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$ - $mlexpr_of_list mlexpr_of_constr l$ >> + $mlexpr_of_pair + (mlexpr_of_list mlexpr_of_constr) + (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >> | Topconstr.CPatVar (loc,n) -> <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" -- cgit v1.2.3