X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=c82f0fb8add1cfa8366d68a4b2740b89f8e25171;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=87944aa34f23a98028573c59c3a445fef78ae1c5;hpb=cbe0302d6b0d2bca6657fa7479a62d0004665612;p=helm.git diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index 87944aa34..c82f0fb8a 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -77,8 +77,10 @@ and countterm current_size t = let size1 = countvar c var in countterm size1 s) current_size l in countterm size1 t - | A.Ident(s,None) -> current_size + (String.length s) - | A.Ident(s,Some l) -> + | A.Ident (s,None) + | A.Uri (s, None) -> current_size + (String.length s) + | A.Ident (s,Some l) + | A.Uri (s,Some l) -> List.fold_left (fun c (v,t) -> countterm (c + (String.length v)) t) (current_size + (String.length s)) l @@ -136,6 +138,12 @@ let append_tail ~tail box = | [] -> box | _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail)) +let rec find_symbol idref = function + | A.AttributedTerm (`Loc _, t) -> find_symbol None t + | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t + | A.Symbol (name, _) -> `Symbol (name, idref) + | _ -> `None + let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) (t, ids_to_uris) = @@ -163,19 +171,10 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) | A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t | A.Appl [] -> assert false | A.Appl ((hd::tl) as l) -> - let rec find_symbol idref = function - | A.AttributedTerm (`Loc _, t) -> find_symbol None t - | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t - | A.Symbol (name, _) -> - (match idref with - | None -> assert false - | Some idref -> `Symbol (name, idref)) - | _ -> `None - in let aattr = make_attributes [Some "helm","xref"] [xref] in (match find_symbol None hd with | `Symbol (name, sxref) -> - let sattr = make_std_attributes (Some sxref) in + let sattr = make_std_attributes sxref in (try (let f = Hashtbl.find symbol_table_charcount name in f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr) @@ -228,14 +227,15 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) Box.smallskip; Box.Text([],map_tex unicode "Rightarrow"); Box.smallskip; - Box.Object([],rhs)]) in - let plbox = match pl with - [] -> Box.Text([],"[]") + append_tail ~tail (Box.Object([],rhs))]) in + let plbox = + match pl with + [] -> append_tail ~tail (Box.Text([],"[]")) | r::tl -> Box.V([], (make_rule ~tail:[] "[" r) :: (make_args - (fun ~tail pat -> make_rule ~tail:[] "|" pat) + (fun ~tail pat -> make_rule ~tail "|" pat) ~tail:("]" :: tail) tl)) in @@ -243,7 +243,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) match ty with | Some ty -> [ Box.H([],[Box.Text([],"["); - ast2box ~tail ty; + ast2box ~tail:[] ty; Box.Text([],"]")]) ] | None -> [] in @@ -251,7 +251,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) Box.V(make_attributes [Some "helm","xref"] [xref], ty_box @ [Box.Text([],"match"); - Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg])); + Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg])); Box.Text([],"with"); Box.indent plbox]) else @@ -260,7 +260,7 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) [Box.H(make_attributes [Some "helm","xref"] [xref], [Box.Text([],"match"); Box.smallskip; - ast2box ~tail arg; + ast2box ~tail:[] arg; Box.smallskip; Box.Text([],"with")]); Box.indent plbox]) @@ -271,14 +271,14 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) let definitions = let rec make_defs let_txt = function [] -> [] - | [(var,s,_)] -> - make_def let_txt var s "in" + | [(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(make_attributes [Some "helm","xref"] [xref], definitions@[ast2box ~tail body]) - | A.Ident (s, subst) -> + | A.Ident (s, subst) + | A.Uri (s, subst) -> let subst = let rec make_substs start_txt = function @@ -423,7 +423,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = | A.Symbol (name,_) -> let attr = make_std_attributes xref in P.Mi (attr,name) - | A.Ident (name,subst) -> + | A.Ident (name,subst) + | A.Uri (name,subst) -> let attr = make_std_attributes xref in let rec make_subst = (function @@ -470,20 +471,10 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = | A.UserInput -> P.Mtext([], "") | A.Appl [] -> assert false | A.Appl ((hd::tl) as l) -> - let rec find_symbol idref = function - | A.AttributedTerm (`Loc _, t) -> find_symbol None t - | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t - | A.Symbol (name, _) -> - (match idref with - | None -> assert false - | Some idref -> `Symbol (name, idref)) - | term -> - `None - in let aattr = make_attributes [Some "helm","xref"] [xref] in (match find_symbol None hd with | `Symbol (name, sxref) -> - let sattr = make_std_attributes (Some sxref) in + let sattr = make_std_attributes sxref in (try (let f = Hashtbl.find symbol_table name in f tl ~priority ~assoc ~ids_to_uris aattr sattr) @@ -547,7 +538,8 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = let lhs = P.Mtext([], constr) :: (List.concat - (List.map (fun var -> P.smallskip :: make_capture_variable var) + (List.map + (fun var -> P.smallskip :: make_capture_variable var) vars)) in lhs @ @@ -693,4 +685,5 @@ let _ = (** fill symbol_table *) add_binary_op "times" 70 (`Ascii "*"); add_binary_op "minus" 60 (`Ascii "-"); add_binary_op "div" 60 (`Ascii "/"); + add_binary_op "cast" 80 (`Ascii ":");