From ae578957a656e46c86a23626b219f4e841734b18 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 May 2009 21:42:45 +0000 Subject: [PATCH] Buffers are now used everywhere for speed-up. However, the ppsubst is deadly slow even for not-that-large substitutions. --- helm/software/components/ng_kernel/nCicPp.ml | 386 ++++++++++--------- 1 file changed, 212 insertions(+), 174 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 47cdfa3ca..27590ed3e 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -13,6 +13,7 @@ module C = NCic module R = NReference +module F = Format let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);; let set_head_beta_reduce = (:=) head_beta_reduce;; @@ -58,205 +59,242 @@ let string_of_implicit_annotation = function | `Typeof x -> "Ty("^string_of_int x^")" ;; -let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t = - let buff = Buffer.create 100 in - let f = Format.formatter_of_buffer buff in - let module F = Format in - let rec aux ?(toplevel=false) ctx = function - | C.Rel m -> - (try - let name = List.nth ctx (m-1) in - F.fprintf f "%s" (if name = "_" then "__"^string_of_int m else name) - with Failure "nth" | Invalid_argument "List.nth" -> - F.fprintf f " -%d" (m - List.length ctx)) - | C.Const r -> F.fprintf f "%s" (r2s inside_fix r) - | C.Prod ("_",s,t) -> - if not toplevel then F.fprintf f "("; - F.fprintf f "@["; - (match s with - | C.Prod ("_",_,_) -> aux ~toplevel:false ctx s - | _ -> aux ~toplevel:true ctx s); - F.fprintf f "@;→ "; - aux ~toplevel:true ("_"::ctx) t; - F.fprintf f "@]"; - if not toplevel then F.fprintf f ")"; - | C.Prod (name,s,t) -> - if not toplevel then F.fprintf f "("; - F.fprintf f "@["; - F.fprintf f "@[∀%s:@;" name; - aux ~toplevel:true ctx s; - F.fprintf f "@].@;"; - aux ~toplevel:true (name::ctx) t; - F.fprintf f "@]"; - if not toplevel then F.fprintf f ")"; - | C.Lambda (name,s,t) -> - if not toplevel then F.fprintf f "("; - F.fprintf f "@["; - F.fprintf f "λ%s:" name; - aux ~toplevel:true ctx s; - F.fprintf f ".@;"; - aux ~toplevel:true (name::ctx) t; - F.fprintf f "@]"; - if not toplevel then F.fprintf f ")"; - | C.LetIn (name,ty,t,b) -> - if not toplevel then F.fprintf f "("; - F.fprintf f "@["; - F.fprintf f "let %s:@;" name; - aux ~toplevel:true ctx ty; - F.fprintf f "@;≝ "; - aux ~toplevel:true ctx t; - F.fprintf f "@;in@;"; - (aux ~toplevel:true (name::ctx) b); - F.fprintf f "@]"; - if not toplevel then F.fprintf f ")"; - | C.Match (r,oty,t,pl) -> - F.fprintf f "@[match "; - aux ~toplevel:true ctx t; - F.fprintf f "@;return "; - aux ~toplevel:true ctx oty; - F.fprintf f "@; @[[ "; - if pl <> [] then - begin - F.fprintf f "@[%s ⇒@;" - (try r2s inside_fix (R.mk_constructor 1 r) - with R.IllFormedReference _ -> "#ERROR#"); - aux ~toplevel:true ctx (List.hd pl); - F.fprintf f "@]"; - ignore(List.fold_left - (fun i t -> - F.fprintf f "@;| @[%s ⇒@;" - (try r2s inside_fix (R.mk_constructor i r) - with R.IllFormedReference _ -> "#ERROR#"); - aux ~toplevel:true ctx t; - F.fprintf f "@]"; - i+1) - 2 (List.tl pl)); - end; - F.fprintf f "]@] @]"; - | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> - F.fprintf f "BAD APPLICATION" - | C.Appl (C.Meta (n,lc) :: args) when List.mem_assoc n subst -> +let ppterm ~formatter:f ~context ~subst ~metasenv:_ ?(inside_fix=false) t = + let rec aux ?(toplevel=false) ctx = function + | C.Rel m -> + (try + let name = List.nth ctx (m-1) in + F.fprintf f "%s" (if name = "_" then "__"^string_of_int m else name) + with Failure "nth" | Invalid_argument "List.nth" -> + F.fprintf f " -%d" (m - List.length ctx)) + | C.Const r -> F.fprintf f "%s" (r2s inside_fix r) + | C.Prod ("_",s,t) -> + if not toplevel then F.fprintf f "("; + F.fprintf f "@["; + (match s with + | C.Prod ("_",_,_) -> aux ~toplevel:false ctx s + | _ -> aux ~toplevel:true ctx s); + F.fprintf f "@;→ "; + aux ~toplevel:true ("_"::ctx) t; + F.fprintf f "@]"; + if not toplevel then F.fprintf f ")"; + | C.Prod (name,s,t) -> + if not toplevel then F.fprintf f "("; + F.fprintf f "@["; + F.fprintf f "@[∀%s:@;" name; + aux ~toplevel:true ctx s; + F.fprintf f "@].@;"; + aux ~toplevel:true (name::ctx) t; + F.fprintf f "@]"; + if not toplevel then F.fprintf f ")"; + | C.Lambda (name,s,t) -> + if not toplevel then F.fprintf f "("; + F.fprintf f "@["; + F.fprintf f "λ%s:" name; + aux ~toplevel:true ctx s; + F.fprintf f ".@;"; + aux ~toplevel:true (name::ctx) t; + F.fprintf f "@]"; + if not toplevel then F.fprintf f ")"; + | C.LetIn (name,ty,t,b) -> + if not toplevel then F.fprintf f "("; + F.fprintf f "@["; + F.fprintf f "let %s:@;" name; + aux ~toplevel:true ctx ty; + F.fprintf f "@;≝ "; + aux ~toplevel:true ctx t; + F.fprintf f "@;in@;"; + (aux ~toplevel:true (name::ctx) b); + F.fprintf f "@]"; + if not toplevel then F.fprintf f ")"; + | C.Match (r,oty,t,pl) -> + F.fprintf f "@[match "; + aux ~toplevel:true ctx t; + F.fprintf f "@;return "; + aux ~toplevel:true ctx oty; + F.fprintf f "@; @[[ "; + if pl <> [] then + begin + F.fprintf f "@[%s ⇒@;" + (try r2s inside_fix (R.mk_constructor 1 r) + with R.IllFormedReference _ -> "#ERROR#"); + aux ~toplevel:true ctx (List.hd pl); + F.fprintf f "@]"; + ignore(List.fold_left + (fun i t -> + F.fprintf f "@;| @[%s ⇒@;" + (try r2s inside_fix (R.mk_constructor i r) + with R.IllFormedReference _ -> "#ERROR#"); + aux ~toplevel:true ctx t; + F.fprintf f "@]"; + i+1) + 2 (List.tl pl)); + end; + F.fprintf f "]@] @]"; + | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) -> + F.fprintf f "BAD APPLICATION" + | C.Appl (C.Meta (n,lc) :: args) when List.mem_assoc n subst -> + let _,_,t,_ = List.assoc n subst in + let hd = NCicSubstitution.subst_meta lc t in + aux ctx + (!head_beta_reduce ~upto:(List.length args) + (match hd with + | NCic.Appl l -> NCic.Appl (l@args) + | _ -> NCic.Appl (hd :: args))) + | C.Appl l -> + F.fprintf f "@["; + if not toplevel then F.fprintf f "("; + aux ctx (List.hd l); + List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l); + if not toplevel then F.fprintf f ")"; + F.fprintf f "@]" + | C.Implicit annot -> + F.fprintf f "?%s" (string_of_implicit_annotation annot) + | C.Meta (n,lc) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in - let hd = NCicSubstitution.subst_meta lc t in - aux ctx - (!head_beta_reduce ~upto:(List.length args) - (match hd with - | NCic.Appl l -> NCic.Appl (l@args) - | _ -> NCic.Appl (hd :: args))) - | C.Appl l -> - F.fprintf f "@["; - if not toplevel then F.fprintf f "("; - aux ctx (List.hd l); - List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l); - if not toplevel then F.fprintf f ")"; - F.fprintf f "@]" - | C.Implicit annot -> - F.fprintf f "?%s" (string_of_implicit_annotation annot) - | C.Meta (n,lc) when List.mem_assoc n subst -> - let _,_,t,_ = List.assoc n subst in - aux ctx (NCicSubstitution.subst_meta lc t) - | C.Meta (n,(shift,C.Irl len)) -> - F.fprintf f "?%d(%d,%d)" n shift len - | C.Meta (n,(shift,C.Ctx l)) -> - F.fprintf f "?%d(%d,[" n shift; - if List.length l > 0 then - begin - aux ctx (NCicSubstitution.lift shift (List.hd l)); - List.iter (fun x -> F.fprintf f ",";aux ctx x) - (List.map (NCicSubstitution.lift shift) (List.tl l)); - end; - F.fprintf f "])" - | C.Sort C.Prop -> F.fprintf f "Prop" - | C.Sort (C.Type []) -> F.fprintf f "Type0" - | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) - | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) - | C.Sort (C.Type l) -> - F.fprintf f "Max("; - aux ctx (C.Sort (C.Type [List.hd l])); - List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) - (List.tl l); - F.fprintf f ")" - in - aux ~toplevel:true (List.map fst context) t; - F.fprintf f "@?"; + aux ctx (NCicSubstitution.subst_meta lc t) + | C.Meta (n,(shift,C.Irl len)) -> + F.fprintf f "?%d(%d,%d)" n shift len + | C.Meta (n,(shift,C.Ctx l)) -> + F.fprintf f "?%d(%d,[" n shift; + if List.length l > 0 then + begin + aux ctx (NCicSubstitution.lift shift (List.hd l)); + List.iter (fun x -> F.fprintf f ",";aux ctx x) + (List.map (NCicSubstitution.lift shift) (List.tl l)); + end; + F.fprintf f "])" + | C.Sort C.Prop -> F.fprintf f "Prop" + | C.Sort (C.Type []) -> F.fprintf f "Type0" + | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) + | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) + | C.Sort (C.Type l) -> + F.fprintf f "Max("; + aux ctx (C.Sort (C.Type [List.hd l])); + List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) + (List.tl l); + F.fprintf f ")" + in + aux ~toplevel:true (List.map fst context) t +;; + +let on_buffer f t = + let buff = Buffer.create 100 in + let formatter = F.formatter_of_buffer buff in + f ~formatter:formatter t; + F.fprintf formatter "@?"; Buffer.contents buff ;; -let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = - Format.set_margin margin; - ppterm ~context ~subst ~metasenv ?inside_fix t +let ppterm ~formatter ~context ~subst ~metasenv ?(margin=80) ?inside_fix t = + F.set_margin margin; + ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t ;; -let rec ppcontext ?(sep="\n") ~subst ~metasenv = function - | [] -> "" +let rec ppcontext ~formatter ?(sep="\n") ~subst ~metasenv = function + | [] -> () | (name, NCic.Decl t) :: tl -> - ppcontext ~sep ~subst ~metasenv tl ^ - name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl t ^ sep + ppcontext ~formatter ~sep ~subst ~metasenv tl; + F.fprintf formatter "%s: " name; + ppterm ~formatter ~subst ~metasenv ~context:tl t; + F.fprintf formatter "%s" sep | (name, NCic.Def (bo,ty)) :: tl-> - ppcontext ~sep ~subst ~metasenv tl ^ - name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl ty ^ - " := " ^ ppterm ~subst ~metasenv ~context:tl bo ^ sep + ppcontext ~formatter ~sep ~subst ~metasenv tl; + F.fprintf formatter "%s: " name; + ppterm ~formatter ~subst ~metasenv ~context:tl ty; + F.fprintf formatter " := "; + ppterm ~formatter ~subst ~metasenv ~context:tl bo; + F.fprintf formatter "%s" sep ;; -let rec ppmetasenv ~subst metasenv = function - | [] -> "" +let rec ppmetasenv ~formatter ~subst metasenv = function + | [] -> () | (i,(name, ctx, ty)) :: tl -> let name = match name with Some n -> "("^n^")" | _ -> "" in - ppcontext ~sep:"; " ~subst ~metasenv ctx ^ - " ⊢ ?"^string_of_int i^name^" : " ^ - ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^ - ppmetasenv ~subst metasenv tl + ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; + F.fprintf formatter " ⊢ ?%d%s : " i name; + ppterm ~formatter ~metasenv ~subst ~context:ctx ty; + F.fprintf formatter "\n"; + ppmetasenv ~formatter ~subst metasenv tl ;; -let ppmetasenv ~subst metasenv = ppmetasenv ~subst metasenv metasenv;; +let ppmetasenv ~formatter ~subst metasenv = + ppmetasenv ~formatter ~subst metasenv metasenv +;; -let rec ppsubst ~subst ~metasenv = function - | [] -> "" +let rec ppsubst ~formatter ~subst ~metasenv = function + | [] -> () | (i,(name, ctx, t, ty)) :: tl -> - let name = match name with Some n -> "("^n^")" | _ -> "" in - ppcontext ~sep:"; " ~subst ~metasenv ctx ^ - " ⊢ ?"^string_of_int i^name^" := " ^ - ppterm ~metasenv ~subst ~context:ctx t ^ " : " ^ - ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^ - ppsubst ~subst ~metasenv tl + ppcontext ~formatter ~sep:"; " ~subst ~metasenv ctx; + F.fprintf formatter " ⊢ ?%d%s := " i name; + ppterm ~formatter ~metasenv ~subst ~context:ctx t; + F.fprintf formatter " : "; + ppterm ~formatter ~metasenv ~subst ~context:ctx ty; + F.fprintf formatter "\n"; + ppsubst ~formatter ~subst ~metasenv tl ;; -let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;; - +let ppsubst ~formatter ~metasenv subst = + ppsubst ~formatter ~metasenv ~subst subst +;; -let ppobj (u,_,metasenv, subst, o) = - "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^ - "subst:\n" ^ ppsubst subst ~metasenv ^ "\n" ^ +let ppobj ~formatter (u,_,metasenv, subst, o) = + F.fprintf formatter "metasenv:\n"; + ppmetasenv ~formatter ~subst metasenv; + F.fprintf formatter "\n"; + F.fprintf formatter "subst:\n"; + (*ppsubst subst ~formatter ~metasenv;*) + F.fprintf formatter "\n"; match o with | NCic.Fixpoint (b, fl, _) -> - "{"^NUri.string_of_uri u^"}\n"^ - (if b then "let rec " else "let corec ") ^ - String.concat "\nand " - (List.map (fun (_,name,n,ty,bo) -> - name^ " on " ^ string_of_int n ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ - ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl) + F.fprintf formatter "{%s}\n" (NUri.string_of_uri u); + F.fprintf formatter "%s" (if b then "let rec " else "let corec "); + HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ") + (fun (_,name,n,ty,bo) -> + F.fprintf formatter "%s on %d : " name n; + ppterm ~formatter ~metasenv ~subst ~context:[] ty; + F.fprintf formatter " :=\n"; + ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl | NCic.Inductive (b, leftno,tyl, _) -> - "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^ - (if b then "inductive " else "coinductive ")^ - String.concat "\nand " - (List.map (fun (_,name,ty,cl) -> - name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^ - String.concat "\n" - (List.map (fun (_,name,ty) -> - " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty) - cl)) tyl) ^ "." + F.fprintf formatter "{%s} with %d fixed params\n%s" + (NUri.string_of_uri u) leftno + (if b then "inductive " else "coinductive "); + HExtlib.list_iter_sep ~sep:(fun ()->F.fprintf formatter "\nand ") + (fun (_,name,ty,cl) -> + F.fprintf formatter "%s: " name; + ppterm ~formatter ~metasenv ~subst ~context:[] ty; + F.fprintf formatter " :=\n"; + HExtlib.list_iter_sep ~sep:(fun () -> F.fprintf formatter "\n") + (fun (_,name,ty) -> + F.fprintf formatter " | %s: " name; + ppterm ~formatter ~metasenv ~subst ~context:[] ty) + cl + ) tyl | NCic.Constant (_,name,None,ty, _) -> - "{"^NUri.string_of_uri u^"}\n"^ - "axiom " ^ name ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ "\n" + F.fprintf formatter "{%s}\naxiom %s : " (NUri.string_of_uri u) name; + ppterm ~formatter ~metasenv ~subst ~context:[] ty; + F.fprintf formatter "\n" | NCic.Constant (_,name,Some bo,ty, _) -> - "{"^NUri.string_of_uri u^"}\n"^ - "definition " ^ name ^ " : " ^ - ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^ - ppterm ~metasenv ~subst ~context:[] bo ^ "\n" + F.fprintf formatter "{%s}\ndefinition %s : " (NUri.string_of_uri u) name; + ppterm ~formatter ~metasenv ~subst ~context:[] ty; + F.fprintf formatter " := \n"; + ppterm ~formatter ~metasenv ~subst ~context:[] bo; + F.fprintf formatter "\n" ;; -let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);; +let ppterm ~context ~subst ~metasenv ?margin ?inside_fix t = + on_buffer (ppterm ~context ~subst ~metasenv ?margin ?inside_fix) t +;; + +let ppcontext ?sep ~subst ~metasenv ctx = + on_buffer (ppcontext ?sep ~subst ~metasenv) ctx +;; +let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;; + +let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;; + +let ppobj obj = on_buffer ppobj obj;; + +let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);; -- 2.39.2