From 3b22e6ed78aa7d1d076734a7e91ef6f2066a4aa9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 17:54:15 +0000 Subject: [PATCH] \Assign and \subst to match the parser. --- helm/ocaml/cic_transformations/ast2pres.ml | 234 ++++++++++----------- 1 file changed, 117 insertions(+), 117 deletions(-) diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index 654135699..9fc2533ae 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -75,19 +75,19 @@ and countterm current_size t = (fun c (var,s,_) -> let size1 = countvar c var in countterm size1 s) current_size l in - countterm size1 t + countterm size1 t | A.Ident(s,None) -> current_size + (String.length s) | A.Ident(s,Some l) -> List.fold_left - (fun c (v,t) -> countterm (c + (String.length v)) t) + (fun c (v,t) -> countterm (c + (String.length v)) t) (current_size + (String.length s)) l | A.Implicit -> current_size + 1 (* underscore *) | A.Meta (_,l) -> - List.fold_left - (fun c t -> + List.fold_left + (fun c t -> match t with - None -> c + 1 (* underscore *) - | Some t -> countterm c t) + None -> c + 1 (* underscore *) + | Some t -> countterm c t) (current_size + 1) l (* num *) | A.Num (s, _) -> current_size + String.length s | A.Sort _ -> current_size + 4 (* sort name *) @@ -103,7 +103,7 @@ let map_attribute = `Loc (n,m) -> (Some "helm","loc",(string_of_int n)^" "^(string_of_int m)) | `IdRef s -> - (Some "helm","xref",s) + (Some "helm","xref",s) ;; let map_attributes = List.map map_attribute @@ -123,53 +123,53 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = A.AttributedTerm (attr1, t) -> (* attr should be empty, since AtrtributedTerm are not supposed to be directly nested *) - bigast2box ~priority ~assoc ~attr:(attr1::~attr) t + bigast2box ~priority ~assoc ~attr:(attr1::~attr) t | A.Appl l -> - Box.H + Box.H (map_attributes attr, - [Box.Text([],"("); + [Box.Text([],"("); Box.V([],List.map ast2box l); Box.Text([],")")]) | A.Binder (`Forall, (Cic.Anonymous, typ), body) | A.Binder (`Pi, (Cic.Anonymous, typ), body) -> - Box.V(map_attributes attr, - [Box.H([],[(match typ with + Box.V(map_attributes attr, + [Box.H([],[(match typ with | None -> Box.Text([], "?") | Some typ -> ast2box typ); - Box.smallskip; + Box.smallskip; Box.Text([], "\\to")]); Box.indent(ast2box body)]) | A.Binder(kind, var, body) -> - Box.V(map_attributes attr, - [Box.H([],[resolve_binder kind; - Box.smallskip; - make_var var; - Box.Text([],".")]); - Box.indent (ast2box body)]) + Box.V(map_attributes attr, + [Box.H([],[resolve_binder kind; + Box.smallskip; + make_var var; + Box.Text([],".")]); + Box.indent (ast2box body)]) | A.Case(arg, _, ty, pl) -> - let make_rule sep ((constr,vars),rhs) = - if (is_big rhs) then - Box.V([],[Box.H([],[Box.Text([],sep); - Box.smallskip; - make_pattern constr vars; - Box.smallskip; - Box.Text([],"\Rightarrow")]); - Box.indent (bigast2box rhs)]) - else - Box.H([],[Box.Text([],sep); - Box.smallskip; - make_pattern constr vars; - Box.smallskip; - Box.Text([],"\Rightarrow"); - Box.smallskip; - Box.Object([],rhs)]) in - let plbox = match pl with - [] -> Box.Text([],"[]") - | r::tl -> - Box.H([], - [Box.V([], - (make_rule "[" r)::(List.map (make_rule "|") tl)); - Box.Text([],"]")]) in + let make_rule sep ((constr,vars),rhs) = + if (is_big rhs) then + Box.V([],[Box.H([],[Box.Text([],sep); + Box.smallskip; + make_pattern constr vars; + Box.smallskip; + Box.Text([],"\Rightarrow")]); + Box.indent (bigast2box rhs)]) + else + Box.H([],[Box.Text([],sep); + Box.smallskip; + make_pattern constr vars; + Box.smallskip; + Box.Text([],"\Rightarrow"); + Box.smallskip; + Box.Object([],rhs)]) in + let plbox = match pl with + [] -> Box.Text([],"[]") + | r::tl -> + Box.H([], + [Box.V([], + (make_rule "[" r)::(List.map (make_rule "|") tl)); + Box.Text([],"]")]) in let ty_box = match ty with | Some ty -> @@ -178,79 +178,79 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) = Box.Text([],"]")]) ] | None -> [] in - if is_big arg then - Box.V(map_attributes attr, + if is_big arg then + Box.V(map_attributes attr, ty_box @ [Box.Text([],"match"); - Box.H([],[Box.skip; - bigast2box arg; - Box.smallskip; - Box.Text([],"with")]); - plbox]) - else - Box.V(map_attributes attr, + Box.H([],[Box.skip; + bigast2box arg; + Box.smallskip; + Box.Text([],"with")]); + plbox]) + else + Box.V(map_attributes attr, ty_box @ - [Box.H(map_attributes attr, - [Box.Text([],"match"); - Box.smallskip; - ast2box arg; - Box.smallskip; - Box.Text([],"with")]); - plbox]) + [Box.H(map_attributes attr, + [Box.Text([],"match"); + Box.smallskip; + ast2box arg; + Box.smallskip; + Box.Text([],"with")]); + plbox]) | A.LetIn (var, s, t) -> - Box.V(map_attributes attr, - (make_def "let" var s "in")@[ast2box t]) + Box.V(map_attributes attr, + (make_def "let" var s "in")@[ast2box t]) | A.LetRec (_, vars, body) -> - let definitions = - let rec make_defs let_txt = function - [] -> [] - | [(var,s,_)] -> - make_def let_txt var s "in" - | (var,s,_)::tl -> - (make_def let_txt var s "")@(make_defs "and" tl) in - make_defs "let rec" vars in - Box.V(map_attributes attr, - definitions@[ast2box body]) + let definitions = + let rec make_defs let_txt = function + [] -> [] + | [(var,s,_)] -> + make_def let_txt var s "in" + | (var,s,_)::tl -> + (make_def let_txt var s "")@(make_defs "and" tl) in + make_defs "let rec" vars in + Box.V(map_attributes attr, + definitions@[ast2box body]) | A.Ident (s, subst) -> - let subst = - let rec make_substs start_txt = - function - [] -> [] - | [(s,t)] -> - make_subst start_txt s t "]" - | (s,t)::tl -> - (make_subst start_txt s t ";")@(make_substs " " tl) + let subst = + let rec make_substs start_txt = + function + [] -> [] + | [(s,t)] -> + make_subst start_txt s t "]" + | (s,t)::tl -> + (make_subst start_txt s t ";")@(make_substs " " tl) in match subst with - | Some subst -> make_substs "[" subst + | Some subst -> make_substs "\\subst [" subst | None -> [] in - Box.V([], (* attr here or on Vbox? *) - [Box.Text(map_attributes attr,s); - Box.indent(Box.V([],subst))]) + Box.V([], (* attr here or on Vbox? *) + [Box.Text(map_attributes attr,s); + Box.indent(Box.V([],subst))]) | A.Implicit -> - Box.Text([],"_") (* big? *) + Box.Text([],"_") (* big? *) | A.Meta (n, l) -> - let local_context = - List.map - (function t -> - Box.H([],[aux_option t; Box.Text([],";")])) - l in - Box.V(map_attributes attr, - [Box.Text([],"?"^(string_of_int n)); - Box.H([],[Box.Text([],"["); - Box.V([],local_context); - Box.Text([],"]")])]) + let local_context = + List.map + (function t -> + Box.H([],[aux_option t; Box.Text([],";")])) + l in + Box.V(map_attributes attr, + [Box.Text([],"?"^(string_of_int n)); + Box.H([],[Box.Text([],"["); + Box.V([],local_context); + Box.Text([],"]")])]) | A.Num (s, _) -> - Box.Text([],s) + Box.Text([],s) | A.Sort kind -> - (match kind with - `Prop -> Box.Text([],"Prop") - | `Set -> Box.Text([],"Set") - | `Type -> Box.Text([],"Type") - | `CProp -> Box.Text([],"CProp")) + (match kind with + `Prop -> Box.Text([],"Prop") + | `Set -> Box.Text([],"Set") + | `Type -> Box.Text([],"Type") + | `CProp -> Box.Text([],"CProp")) | A.Symbol (s, _) -> - Box.Text([],s) + Box.Text([],s) and aux_option = function None -> Box.Text([],"_") @@ -263,32 +263,32 @@ and make_var = function | (Cic.Name s, None) -> Box.Text([],s) | (Cic.Name s, Some t) -> if is_big t then - Box.V([],[Box.Text([],s^":"); - Box.indent(bigast2box t)]) + Box.V([],[Box.Text([],s^":"); + Box.indent(bigast2box t)]) else - Box.H([],[Box.Text([],s^":");Box.Object([],t)]) + Box.H([],[Box.Text([],s^":");Box.Object([],t)]) and make_pattern constr = function [] -> Box.Text([],constr) | vars -> - let bvars = - List.fold_right - (fun var acc -> - let bv = - match var with - (* ignoring the type *) - (Cic.Anonymous, _) -> Box.Text([],"_") - | (Cic.Name s, _) -> Box.Text([],s) in - Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in - Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars) + let bvars = + List.fold_right + (fun var acc -> + let bv = + match var with + (* ignoring the type *) + (Cic.Anonymous, _) -> Box.Text([],"_") + | (Cic.Name s, _) -> Box.Text([],s) in + Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in + Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars) and make_def let_txt var def end_txt = let name = (match var with (* ignoring the type *) - (Cic.Anonymous, _) -> Box.Text([],"_") + (Cic.Anonymous, _) -> Box.Text([],"_") | (Cic.Name s, _) -> Box.Text([],s)) in pretty_append [Box.Text([],let_txt); @@ -305,11 +305,11 @@ and make_subst start_txt varname body end_txt = [Box.Text([],start_txt); Box.Text([],varname); Box.smallskip; - Box.Text([],":=") + Box.Text([],"\Assign") ] body [Box.Text([],end_txt)] - + and pretty_append l ast tail = prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast)); if is_big ast then @@ -320,7 +320,7 @@ and pretty_append l ast tail = ;; - + -- 2.39.2