From: Andrea Asperti Date: Mon, 26 Jan 2004 13:40:46 +0000 (+0000) Subject: Notation for Case revisited and completed. X-Git-Tag: V_0_2_3~139 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bafecec2d4af08af32249b4ec75db477a6024c7b;p=helm.git Notation for Case revisited and completed. --- diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml index 0b303083d..5210840c8 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -33,58 +33,56 @@ (**************************************************************************) module P = Mpresentation;; +module CE = Content_expressions;; let symbol_table = Hashtbl.create 503;; let symbol_table_charcount = Hashtbl.create 503;; let maxsize = 25;; -let countterm current_size t = - let module CE = Content_expressions in - let rec aux current_size t = - if current_size > maxsize then current_size - else match t with - CE.Symbol (_,name,None,_) -> current_size + (String.length name) - | CE.Symbol (_,name,Some subst,_) -> - let c1 = current_size + (String.length name) in - countsubst subst c1 - | CE.LocalVar (_,name) -> current_size + (String.length name) - | CE.Meta (_,name,l) -> - List.fold_left - (fun i t -> - match t with - None -> i - | Some t' -> aux i t' - ) (current_size + String.length name) l - | CE.Num (_,value) -> current_size + (String.length value) - | CE.Appl (_,l) -> - List.fold_left aux current_size l - | CE.Binder (_, _,(n,s),body) -> - let cs = aux (current_size + 2 + (String.length n)) s in - aux cs body - | CE.Letin (_,(n,s),body) -> - let cs = aux (current_size + 3 + (String.length n)) s in - aux cs body - | CE.Letrec (_,defs,body) -> - let cs = - List.fold_left - (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size defs in - aux cs body - | CE.Case (_,a,np) -> - let cs = aux (current_size + 4) a in +let rec countterm current_size t = + if current_size > maxsize then current_size + else match t with + CE.Symbol (_,name,None,_) -> current_size + (String.length name) + | CE.Symbol (_,name,Some subst,_) -> + let c1 = current_size + (String.length name) in + countsubst subst c1 + | CE.LocalVar (_,name) -> current_size + (String.length name) + | CE.Meta (_,name,l) -> + List.fold_left + (fun i t -> + match t with + None -> i + | Some t' -> countterm i t' + ) (current_size + String.length name) l + | CE.Num (_,value) -> current_size + (String.length value) + | CE.Appl (_,l) -> + List.fold_left countterm current_size l + | CE.Binder (_, _,(n,s),body) -> + let cs = countterm (current_size + 2 + (String.length n)) s in + countterm cs body + | CE.Letin (_,(n,s),body) -> + let cs = countterm (current_size + 3 + (String.length n)) s in + countterm cs body + | CE.Letrec (_,defs,body) -> + let cs = List.fold_left - (fun c (n,bo) -> aux (c+(String.length n)) bo) current_size np - and - countsubst subst current_size = + (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size defs in + countterm cs body + | CE.Case (_,a,np) -> + let cs = countterm (current_size + 4) a in + List.fold_left + (fun c (n,bo) -> countterm (c+(String.length n)) bo) current_size np + +and +countsubst subst current_size = List.fold_left (fun current_size (uri,expr) -> if (current_size > maxsize) then current_size else let c1 = (current_size + (String.length (UriManager.name_of_uri uri))) in - (aux c1 expr)) current_size subst - in - (aux current_size t) + (countterm c1 expr)) current_size subst ;; let is_big t = @@ -218,16 +216,29 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = let rec make_patterns = (function [] -> [] - | [(n,p)] -> - [P.Mtext([],(n ^ " -> "));(aux p)] + | [(n,p)] -> make_pattern n p | (n,p)::tl -> - P.Mtext([],(n ^ " -> ")):: - (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in + (make_pattern n p)@(P.smallskip:: + P.Mtext([],"|")::P.smallskip::(make_patterns tl))) + and make_pattern n p = + let rec get_vars_and_body = + (function + CE.Binder (_, "Lambda",(n,_),body) -> + let v,b = get_vars_and_body body in + n::v,b + | t -> [],t) in + let vars,body = get_vars_and_body p in + let lhs = + match vars with + [] -> n ^ " -> " + | l -> "(" ^ n ^" "^(String.concat " " l) ^ ")" ^ " -> " in + [P.Mtext([],lhs);P.smallskip;aux body] in P.Mrow (attr, - P.Mtext([],("case ")):: - (aux a):: - P.Mtext([],(" of ")):: - (make_patterns np)@tail) in + P.Mtext([],"match")::P.smallskip:: + (aux a)::P.smallskip:: + P.Mtext([],"with")::P.smallskip:: + P.Mtext([],"[")::P.smallskip:: + (make_patterns np)@(P.smallskip::P.Mtext([],("]"))::tail)) in aux t and @@ -269,10 +280,9 @@ let rec make_args_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) = and cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = - let module CE = Content_expressions in - let module P = Mpresentation in - let rec aux = - function + if not(is_big t) then (cexpr2pres ~priority ~assoc ~tail t) + else let aux = cexpr2pres_charcount in + match t with CE.Symbol (xref,name,None,uri) -> let attr = make_attributes @@ -330,64 +340,56 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = | CE.Appl (axref,CE.Symbol(sxref,n,subst,uri)::tl) -> let aattr = make_attributes [Some "helm","xref"] [axref] in let sattr = make_attributes [Some "helm","xref";Some "xlink","href"] [sxref;uri] in - if (is_big t) then - (try - (let f = Hashtbl.find symbol_table_charcount n in - f tl ~priority ~assoc ~tail aattr sattr) - with notfound -> - P.Mtable (aattr@P.standard_tbl_attr, - P.Mtr([],[P.Mtd([],P.Mrow([], - [P.Mtext([],"("); - cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))]):: - make_args_charcount ~tail:(P.Mtext([],")")::tail) tl)) - else cexpr2pres t - | CE.Appl (xref,l) as t -> - let attr = make_attributes [Some "helm","xref"] [xref] in - if (is_big t) then - P.Mtable (attr@P.standard_tbl_attr, + (try + (let f = Hashtbl.find symbol_table_charcount n in + f tl ~priority ~assoc ~tail aattr sattr) + with notfound -> + P.Mtable (aattr@P.standard_tbl_attr, P.Mtr([],[P.Mtd([],P.Mrow([], [P.Mtext([],"("); - cexpr2pres_charcount (List.hd l)]))]):: - make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l)) - else cexpr2pres t + cexpr2pres (CE.Symbol(sxref,n,subst,uri))]))]):: + make_args_charcount ~tail:(P.Mtext([],")")::tail) tl)) + | CE.Appl (xref,l) as t -> + let attr = make_attributes [Some "helm","xref"] [xref] in + P.Mtable (attr@P.standard_tbl_attr, + P.Mtr([],[P.Mtd([],P.Mrow([], + [P.Mtext([],"("); + cexpr2pres_charcount (List.hd l)]))]):: + make_args_charcount ~tail:(P.Mtext([],")")::tail) (List.tl l)) | CE.Binder (xref, kind,(n,s),body) as t -> - if (is_big t) then - let attr = make_attributes [Some "helm","xref"] [xref] in - let binder = - if kind = "Lambda" then - Netconversion.ustring_of_uchar `Enc_utf8 0x03bb - else if kind = "Prod" then - Netconversion.ustring_of_uchar `Enc_utf8 0x03a0 - else if kind = "Forall" then - Netconversion.ustring_of_uchar `Enc_utf8 0x2200 - else if kind = "Exists" then - Netconversion.ustring_of_uchar `Enc_utf8 0x2203 - else "unknown" in - P.Mtable (attr@P.standard_tbl_attr, - [P.Mtr ([],[P.Mtd ([], - P.Mrow([], - [P.Mtext([None,"mathcolor","Blue"],binder); - P.Mtext([],n ^ ":"); - cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]); - P.Mtr ([],[P.Mtd ([], - P.indented (cexpr2pres_charcount body ~tail:tail))])]) - else (cexpr2pres t ~tail:tail) + let attr = make_attributes [Some "helm","xref"] [xref] in + let binder = + if kind = "Lambda" then + Netconversion.ustring_of_uchar `Enc_utf8 0x03bb + else if kind = "Prod" then + Netconversion.ustring_of_uchar `Enc_utf8 0x03a0 + else if kind = "Forall" then + Netconversion.ustring_of_uchar `Enc_utf8 0x2200 + else if kind = "Exists" then + Netconversion.ustring_of_uchar `Enc_utf8 0x2203 + else "unknown" in + P.Mtable (attr@P.standard_tbl_attr, + [P.Mtr ([],[P.Mtd ([], + P.Mrow([], + [P.Mtext([None,"mathcolor","Blue"],binder); + P.Mtext([],n ^ ":"); + cexpr2pres_charcount s ~tail:[P.Mtext([],".")]]))]); + P.Mtr ([],[P.Mtd ([], + P.indented (cexpr2pres_charcount body ~tail:tail))])]) | CE.Letin (xref,(n,s),body) as t -> - if (is_big t) then - let attr = make_attributes [Some "helm","xref"] [xref] in - P.Mtable (attr@P.standard_tbl_attr, - [P.Mtr ([],[P.Mtd ([], - P.Mrow([], - [P.Mtext([None,"mathcolor","Blue"],"let"); - P.smallskip; - P.Mtext([],n ^ "="); - cexpr2pres_charcount s; - P.smallskip; - P.Mtext([],"in"); - ]))]); - P.Mtr ([],[P.Mtd ([], - P.indented (cexpr2pres_charcount body))])]) - else (cexpr2pres t) + let attr = make_attributes [Some "helm","xref"] [xref] in + P.Mtable (attr@P.standard_tbl_attr, + [P.Mtr ([],[P.Mtd ([], + P.Mrow([], + [P.Mtext([None,"mathcolor","Blue"],"let"); + P.smallskip; + P.Mtext([],n ^ "="); + cexpr2pres_charcount s; + P.smallskip; + P.Mtext([],"in"); + ]))]); + P.Mtr ([],[P.Mtd ([], + P.indented (cexpr2pres_charcount body))])]) | CE.Letrec (xref,defs,body) -> let attr = make_attributes [Some "helm","xref"] [xref] in let rec make_defs = @@ -405,18 +407,54 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = (aux body)]) | CE.Case (xref,a,np) -> let attr = make_attributes [Some "helm","xref"] [xref] in - let rec make_patterns = - (function - [] -> [] - | [(n,p)] -> - [P.Mtext([],(n ^ " -> "));(aux p)] - | (n,p)::tl -> - P.Mtext([],(n ^ " -> ")):: - (aux p)::P.Mtext([]," | ")::(make_patterns tl)) in - P.Mrow (attr, - P.Mtext([],("case ")):: - (aux a):: - P.Mtext([],(" of ")):: - (make_patterns np)) in - aux t + let arg = + if (is_big a) then + let tail = P.Mtext([],(" with"))::tail in + [P.Mtr ([],[P.Mtd ([],P.Mtext([],("match ")))]); + P.Mtr ([],[P.Mtd ([],aux a ~tail:tail)])] + else + [P.Mtr ([],[P.Mtd ([],P.Mrow([],[P.Mtext([],("match"));P.smallskip;aux a ~tail:tail; P.smallskip;P.Mtext([],("with"))]))])] in + let rec make_patterns is_first ~tail = + function + [] -> [] + | [(n,p)] -> + let sep = + if is_first then "[ " else "| " in + [P.Mtr ([], + [P.Mtd ([], + make_pattern sep ~tail n p)])] + | (n,p)::tl -> + let sep = + if is_first then "[ " else "| " in + P.Mtr ([], + [P.Mtd ([], + make_pattern sep [] n p)]) + ::(make_patterns false ~tail tl) + and make_pattern sep ~tail n p = + let rec get_vars_and_body = + function + CE.Binder (_, "Lambda",(n,_),body) -> + let v,b = get_vars_and_body body in + n::v,b + | t -> [],t in + let vars,body = get_vars_and_body p in + let lhs = + match vars with + [] -> sep ^ n ^ " -> " + | l -> sep ^"(" ^n^" "^(String.concat " " l) ^ ")" ^ " -> " in + if (is_big body) then + P.Mtable (P.standard_tbl_attr, + [P.Mtr ([], + [P.Mtd ([],P.Mtext([],lhs))]); + P.Mtr ([], + [P.Mtd ([],P.indented (aux ~tail body ))])]) + else + P.Mrow([],[P.Mtext([],lhs);aux ~tail body]) in + let patterns = + make_patterns true np ~tail:(P.Mtext([],"]")::tail) in + P.Mtable (attr@P.standard_tbl_attr, + arg@patterns) ;; + + +