From: Stefano Zacchiroli Date: Tue, 27 Sep 2005 14:17:34 +0000 (+0000) Subject: Better handling of idref propagation, no more Href hack, multiple idrefs are X-Git-Tag: V_0_7_2_3~296 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3065dd135001f868c677ee181d8a1fa3d498866a;p=helm.git Better handling of idref propagation, no more Href hack, multiple idrefs are now kept at the Ast level. Still issues in idref propagation for magics. --- diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 318361c44..7b85b96b5 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -55,6 +55,8 @@ sig val classify : pattern_t -> pattern_kind val tag_of_pattern : pattern_t -> tag_t * pattern_t list val tag_of_term : term_t -> tag_t * term_t list + val string_of_term: term_t -> string + val string_of_pattern: pattern_t -> string end module Matcher (P: PATTERN) = @@ -117,40 +119,43 @@ struct t let variable_closure ksucc = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "variable_closure"; *) match terms with - | hd :: tl -> ksucc (hd :: matched_terms) tl + | hd :: tl -> ksucc (hd :: matched_terms) constructors tl | _ -> assert false) let success_closure ksucc = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "success_closure"; *) - ksucc matched_terms) + ksucc matched_terms constructors) let constructor_closure ksuccs = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "constructor_closure"; *) match terms with | t :: tl -> (try let tag, subterms = P.tag_of_term t in + let constructors' = + if subterms = [] then t :: constructors else constructors + in let k' = List.assoc tag ksuccs in - k' matched_terms (subterms @ tl) + k' matched_terms constructors' (subterms @ tl) with Not_found -> None) | [] -> assert false) let backtrack_closure ksucc kfail = - (fun matched_terms terms -> + (fun matched_terms constructors terms -> (* prerr_endline "backtrack_closure"; *) - match ksucc matched_terms terms with + match ksucc matched_terms constructors terms with | Some x -> Some x - | None -> kfail matched_terms terms) + | None -> kfail matched_terms constructors terms) let compiler rows match_cb fail_k = let rec aux t = if t = [] then - (fun _ _ -> fail_k ()) + (fun _ _ _ -> fail_k ()) else if are_empty t then success_closure (match_cb (matched t)) else @@ -186,7 +191,7 @@ struct in let t = List.map (fun (p, pid) -> [], [p], pid) rows in let matcher = aux t in - (fun term -> matcher [] [term]) + (fun term -> matcher [] [] [term]) end module Matcher21 = @@ -204,6 +209,8 @@ struct | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag let tag_of_term t = CicNotationTag.get_tag t + let string_of_term = CicNotationPp.pp_term + let string_of_pattern = CicNotationPp.pp_term end module M = Matcher (Pattern21) @@ -254,27 +261,27 @@ struct List.fold_left (fun f (name, m) -> let m_checker = compile_magic m in - (fun env -> - match m_checker (Env.lookup_term env name) env with + (fun env ctors -> + match m_checker (Env.lookup_term env name) env ctors with | None -> None - | Some env' -> f env')) - (fun env -> Some env) + | Some (env, ctors) -> f env ctors)) + (fun env ctors -> Some (env, ctors)) map in let magichooser candidates = List.fold_left (fun f (pid, pl, checker) -> - (fun matched_terms -> + (fun matched_terms constructors -> let env = env_of_matched pl matched_terms in - match checker env with - | None -> f matched_terms - | Some env -> + match checker env constructors with + | None -> f matched_terms constructors + | Some (env, ctors') -> let magic_map = try List.assoc pid magic_maps with Not_found -> assert false in let env' = Env.remove_names env (List.map fst magic_map) in - Some (env', pid))) - (fun _ -> None) + Some (env', ctors', pid))) + (fun _ _ -> None) (List.rev candidates) in let match_cb rows = @@ -298,29 +305,34 @@ struct let acc_name = try List.hd names with Failure _ -> assert false in let compiled_base = compiler [p_base, 0] and compiled_rec = compiler [p_rec, 0] in - (fun term env -> + (fun term env ctors -> let aux_base term = match compiled_base term with | None -> None - | Some (env', _) -> Some (env', []) + | Some (env', ctors', _) -> Some (env', ctors', []) in let rec aux term = match compiled_rec term with | None -> aux_base term - | Some (env', _) -> + | Some (env', ctors', _) -> begin let acc = Env.lookup_term env' acc_name in let env'' = Env.remove_name env' acc_name in match aux acc with | None -> aux_base term - | Some (base_env, rec_envl) -> - Some (base_env, env'' :: rec_envl) + | Some (base_env, ctors', rec_envl) -> + let ctors'' = ctors' @ ctors in + Some (base_env, ctors'',env'' :: rec_envl) end in match aux term with | None -> None - | Some (base_env, rec_envl) -> - Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *) + | Some (base_env, ctors, rec_envl) -> + let env' = + base_env @ Env.coalesce_env p_rec_decls rec_envl @ env + (* @ env LUCA!!! *) + in + Some (env', ctors)) | Ast.Default (p_some, p_none) -> (* p_none can't bound names *) let p_some_decls = Env.declarations_of_term p_some in @@ -332,10 +344,10 @@ struct in let none_env = List.map Env.opt_binding_of_name p_opt_decls in let compiled = compiler [p_some, 0] in - (fun term env -> + (fun term env ctors -> match compiled term with - | None -> Some none_env (* LUCA: @ env ??? *) - | Some (env', 0) -> + | None -> Some (none_env, ctors) (* LUCA: @ env ??? *) + | Some (env', ctors', 0) -> let env' = List.map (fun (name, (ty, v)) as binding -> @@ -344,24 +356,24 @@ struct else binding) env' in - Some (env' @ env) + Some (env' @ env, ctors' @ ctors) | _ -> assert false) | Ast.If (p_test, p_true, p_false) -> let compiled_test = compiler [p_test, 0] and compiled_true = compiler [p_true, 0] and compiled_false = compiler [p_false, 0] in - (fun term env -> + (fun term env ctors -> let branch = match compiled_test term with - | None -> compiled_false - | Some _ -> compiled_true + | None -> compiled_false + | Some _ -> compiled_true in - match branch term with - | None -> None - | Some (env', _) -> Some (env' @ env)) + match branch term with + | None -> None + | Some (env', ctors', _) -> Some (env' @ env, ctors' @ ctors)) - | Ast.Fail -> (fun _ _ -> None) + | Ast.Fail -> (fun _ _ _ -> None) | _ -> assert false end @@ -402,6 +414,9 @@ struct type pattern_t = Ast.cic_appl_pattern type term_t = Cic.annterm + let string_of_pattern = GrafiteAstPp.pp_cic_appl_pattern + let string_of_term t = CicPp.ppterm (Deannotate.deannotate_term t) + let classify = function | Ast.ImplicitPattern | Ast.VarPattern _ -> Variable @@ -414,7 +429,7 @@ struct let compiler rows = let match_cb rows = let pl, pid = try List.hd rows with Not_found -> assert false in - (fun matched_terms -> + (fun matched_terms constructors -> let env = try List.map2 @@ -426,7 +441,7 @@ struct pl matched_terms with Invalid_argument _ -> assert false in - Some (env, pid)) + Some (env, constructors, pid)) in M.compiler rows match_cb (fun () -> None) end diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli index 4a9d4a275..f8daca798 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.mli +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -30,31 +30,50 @@ module type PATTERN = sig type pattern_t type term_t + val classify : pattern_t -> pattern_kind val tag_of_pattern : pattern_t -> tag_t * pattern_t list val tag_of_term : term_t -> tag_t * term_t list + + (** {3 Debugging} *) + val string_of_term: term_t -> string + val string_of_pattern: pattern_t -> string end module Matcher (P: PATTERN) : sig + (** @param patterns pattern matrix (pairs ) + * @param success_cb callback invoked in case of matching. + * Its argument are the list of pattern who matches the input term, the list + * of terms bound in them, the list of terms which matched constructors. + * Its return value is Some _ if the matching is valid, None otherwise; the + * latter kind of return value will trigger backtracking in the pattern + * matching algorithm + * @param failure_cb callback invoked in case of matching failure + * @param term term on which pattern match on *) val compiler: (P.pattern_t * int) list -> - ((P.pattern_t list * int) list -> P.term_t list -> 'a option) -> + ((P.pattern_t list * int) list -> P.term_t list -> P.term_t list -> + 'a option) -> (* terms *) (* constructors *) (unit -> 'a option) -> (P.term_t -> 'a option) end module Matcher21: sig + (** @param l2_patterns level 2 (AST) patterns *) val compiler : (CicNotationPt.term * int) list -> - (CicNotationPt.term -> (CicNotationEnv.t * int) option) + (CicNotationPt.term -> + (CicNotationEnv.t * CicNotationPt.term list * int) option) end module Matcher32: sig + (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) val compiler : (CicNotationPt.cic_appl_pattern * int) list -> - (Cic.annterm -> ((string * Cic.annterm) list * int) option) + (Cic.annterm -> + ((string * Cic.annterm) list * Cic.annterm list * int) option) end diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 1c3ad4386..0bda68846 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -55,12 +55,13 @@ let pp_literal = let rec pp_term ?(pp_parens = true) t = let t_pp = match t with - | Ast.AttributedTerm (`Href hrefs, term) when debug_printing -> - sprintf "#(%s)[%s]" - (String.concat "," (List.map UriManager.string_of_uri hrefs)) - (pp_term ~pp_parens:false term) | Ast.AttributedTerm (`IdRef id, term) when debug_printing -> sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term) + | Ast.AttributedTerm (`XmlAttrs attrs, term) when debug_printing -> + sprintf "X(%s)[%s]" + (String.concat ";" + (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) + (pp_term ~pp_parens:false term) | Ast.AttributedTerm (_, term) when debug_printing -> sprintf "@[%s]" (pp_term ~pp_parens:false term) | Ast.AttributedTerm (`Raw text, _) -> text diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index c4679bef7..34c4c6520 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -38,11 +38,10 @@ let to_unicode = Utf8Macro.unicode_of_tex let rec make_attributes l1 = function | [] -> [] | hd :: tl -> - (match !hd with + (match hd with | None -> make_attributes (List.tl l1) tl | Some s -> let p,n = List.hd l1 in - hd := None; (p,n,s) :: make_attributes (List.tl l1) tl) let box_of_mpres = @@ -203,49 +202,75 @@ let render ids_to_uris = let module A = Ast in let module P = Mpresentation in let use_unicode = true in - let lookup_uri = function - | None -> None - | Some id -> (try Some (Hashtbl.find ids_to_uris id) with Not_found -> None) + let lookup_uri id = + (try + let uri = Hashtbl.find ids_to_uris id in + Some uri + with Not_found -> None) in - let make_href xmlattrs xref uris = - let xref_uri = lookup_uri !xref in - let raw_uris = List.map UriManager.string_of_uri !uris in - let uri = - match xref_uri, raw_uris with - | None, [] -> None - | Some uri, [] -> Some uri - | None, raw_uris -> Some (String.concat " " raw_uris) - | Some uri, raw_uris -> Some (String.concat " " (uri :: raw_uris)) + let make_href xmlattrs xref = + let xref_uris = + List.fold_right + (fun xref uris -> + match lookup_uri xref with + | None -> uris + | Some uri -> uri :: uris) + !xref [] in - uris := []; + let xmlattrs_uris, xmlattrs = + let xref_attrs, other_attrs = + List.partition + (function Some "xlink", "href", _ -> true | _ -> false) + xmlattrs + in + List.map (fun (_, _, uri) -> uri) xref_attrs, + other_attrs + in + let uris = + match xmlattrs_uris @ xref_uris with + | [] -> None + | uris -> + Some (String.concat " " + (HExtlib.list_uniq (List.sort String.compare uris))) + in + let xrefs = + match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs) + in + xref := []; xmlattrs @ make_attributes [Some "helm", "xref"; Some "xlink", "href"] - [xref; ref uri] + [xrefs; uris] + in + let make_xref xref = + let xrefs = + match !xref with [] -> None | xrefs -> Some (String.concat " " xrefs) + in + xref := []; + make_attributes [Some "helm","xref"] [xrefs] in - let make_xref xref = make_attributes [Some "helm","xref"] [xref] in (* when mathonly is true no boxes should be generated, only mrows *) (* "xref" is *) - let rec aux xmlattrs mathonly xref pos prec uris t = + let rec aux xmlattrs mathonly xref pos prec t = match t with | A.AttributedTerm _ -> - aux_attributes xmlattrs mathonly xref pos prec uris t + aux_attributes xmlattrs mathonly xref pos prec t | A.Num (literal, _) -> let attrs = (RenderingAttrs.number_attributes `MathML) - @ make_href xmlattrs xref uris + @ make_href xmlattrs xref in Mpres.Mn (attrs, literal) | A.Symbol (literal, _) -> let attrs = (RenderingAttrs.symbol_attributes `MathML) - @ make_href xmlattrs xref uris + @ make_href xmlattrs xref in Mpres.Mo (attrs, to_unicode literal) | A.Ident (literal, subst) | A.Uri (literal, subst) -> let attrs = (RenderingAttrs.ident_attributes `MathML) - @ make_href xmlattrs xref uris + @ make_href xmlattrs xref in let name = Mpres.Mi (attrs, to_unicode literal) in (match subst with @@ -261,35 +286,23 @@ let render ids_to_uris = box_of mathonly (A.H, false, false) [] [ Mpres.Mi ([], name); Mpres.Mo ([], to_unicode "\\def"); - aux [] mathonly xref pos prec uris t ]) + aux [] mathonly xref pos prec t ]) substs)) @ [ closed_brace ]) -(* (CicNotationUtil.dress semicolon - (List.map - (fun (var, t) -> - let var_uri = UriManager.uri_of_string var in - let var_name = UriManager.name_of_uri var_uri in - let href_attr = Some "xlink", "href", var in - box_of mathonly (A.H, false, false) [] [ - Mpres.Mi ([href_attr], var_name); - Mpres.Mo ([], to_unicode "\\def"); - aux [] mathonly xref pos prec uris t ]) - substs)) *) in let substs_maction = toggle_action [ hidden_substs; substs' ] in box_of mathonly (A.H, false, false) [] [ name; substs_maction ]) - | A.Literal l -> aux_literal xmlattrs xref prec uris l + | A.Literal l -> aux_literal xmlattrs xref prec l | A.UserInput -> Mpres.Mtext ([], "%") - | A.Layout l -> aux_layout mathonly xref pos prec uris l + | A.Layout l -> aux_layout mathonly xref pos prec l | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); assert false - and aux_attributes xmlattrs mathonly xref pos prec uris t = + and aux_attributes xmlattrs mathonly xref pos prec t = let new_level = ref None in - let new_xref = ref None in - let new_uris = ref [] in + let new_xref = ref [] in let new_xmlattrs = ref [] in let rec aux_attribute = function @@ -299,65 +312,58 @@ let render ids_to_uris = | `Raw _ -> () | `Level (child_prec, child_assoc) -> new_level := Some (child_prec, child_assoc) - | `IdRef xref -> new_xref := Some xref - | `Href hrefs -> new_uris := hrefs - | `XmlAttrs attrs -> new_xmlattrs := attrs); + | `IdRef xref -> new_xref := xref :: !new_xref + | `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs); aux_attribute t | t -> (match !new_level with - | None -> aux !new_xmlattrs mathonly new_xref pos prec new_uris t + | None -> aux !new_xmlattrs mathonly new_xref pos prec t | Some (child_prec, child_assoc) -> let t' = - aux !new_xmlattrs mathonly new_xref pos child_prec new_uris t + aux !new_xmlattrs mathonly new_xref pos child_prec t in add_parens child_prec child_assoc pos prec t') in aux_attribute t -(* function - | `Loc _ - | `Raw _ -> aux xmlattrs mathonly xref pos prec uris t - | `Level (child_prec, child_assoc) -> - let t' = aux xmlattrs mathonly xref pos child_prec uris t in - add_parens child_prec child_assoc pos prec t' - | `IdRef xref -> aux xmlattrs mathonly (Some xref) pos prec uris t - | `Href uris' -> aux xmlattrs mathonly xref pos prec uris' t - | `XmlAttrs xmlattrs -> aux xmlattrs mathonly xref pos prec uris t *) - and aux_literal xmlattrs xref prec uris l = - let attrs = make_href xmlattrs xref uris in + and aux_literal xmlattrs xref prec l = + let attrs = make_href xmlattrs xref in (match l with | `Symbol s -> Mpres.Mo (attrs, to_unicode s) | `Keyword s -> Mpres.Mo (attrs, to_unicode s) | `Number s -> Mpres.Mn (attrs, to_unicode s)) - and aux_layout mathonly xref pos prec uris l = + and aux_layout mathonly xref pos prec l = let attrs = make_xref xref in - let invoke' t = aux [] true (ref None) pos prec uris t in + let invoke' t = aux [] true (ref []) pos prec t in (* use the one below to reset precedence and associativity *) - let invoke_reinit t = aux [] true (ref None) `None 0 uris t in + let invoke_reinit t = aux [] true (ref []) `None 0 t in match l with | A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2) | A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2) | A.Below (t1, t2) -> Mpres.Munder (attrs, invoke' t1, invoke_reinit t2) | A.Above (t1, t2) -> Mpres.Mover (attrs, invoke' t1, invoke_reinit t2) | A.Frac (t1, t2) - | A.Over (t1, t2) -> Mpres.Mfrac (attrs, invoke_reinit t1, invoke_reinit t2) + | A.Over (t1, t2) -> + Mpres.Mfrac (attrs, invoke_reinit t1, invoke_reinit t2) | A.Atop (t1, t2) -> - Mpres.Mfrac(atop_attributes @ attrs, invoke_reinit t1, invoke_reinit t2) + Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1, + invoke_reinit t2) | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t) - | A.Root (t1, t2) -> Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2) + | A.Root (t1, t2) -> + Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2) | A.Box ((_, spacing, _) as kind, terms) -> let children = - aux_children mathonly spacing xref pos prec uris + aux_children mathonly spacing xref pos prec (CicNotationUtil.ungroup terms) in box_of mathonly kind attrs children | A.Group terms -> let children = - aux_children mathonly false xref pos prec uris + aux_children mathonly false xref pos prec (CicNotationUtil.ungroup terms) in box_of mathonly (A.H, false, false) attrs children | A.Break -> assert false (* TODO? *) - and aux_children mathonly spacing xref pos prec uris terms = + and aux_children mathonly spacing xref pos prec terms = let find_clusters = let rec aux_list first clusters acc = function @@ -379,7 +385,7 @@ let render ids_to_uris = | `Left -> `Inner in aux_list false clusters - (aux [] mathonly xref pos' prec uris hd :: acc) [] + (aux [] mathonly xref pos' prec hd :: acc) [] | hd :: tl -> let pos' = match pos, first with @@ -391,7 +397,7 @@ let render ids_to_uris = | `Inner, _ -> `Inner in aux_list false clusters - (aux [] mathonly xref pos' prec uris hd :: acc) tl + (aux [] mathonly xref pos' prec hd :: acc) tl in aux_list true [] [] in @@ -402,7 +408,7 @@ let render ids_to_uris = in List.map boxify_pres (find_clusters terms) in - aux [] false (ref None) `None 0 (ref []) + aux [] false (ref []) `None 0 let rec print_box (t: boxml_markup) = Box.box2xml print_mpres t diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index b0e9762be..1dc634930 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -44,7 +44,6 @@ type href = UriManager.uri type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) - | `Href of href list (* hyperlinks for literals *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 6340d88a1..ddf429db6 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -80,7 +80,8 @@ let rec remove_level_info = | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) | t -> t -let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t) +let add_xml_attrs attrs t = + if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) let add_keyword_attrs = add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) @@ -106,7 +107,9 @@ let ident i = let ident_w_href href i = match href with | None -> ident i - | Some href -> Ast.AttributedTerm (`Href [href], ident i) + | Some href -> + let href = UriManager.string_of_uri href in + add_xml_attrs [Some "xlink", "href", href] (ident i) let binder_symbol s = add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) @@ -269,7 +272,8 @@ let pp_ast0 t k = let ast_of_acic0 term_info acic k = let k = k term_info in - let register_uri id uri = Hashtbl.add term_info.uri id uri in + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in let sort_of_id id = try Hashtbl.find term_info.sort id @@ -418,11 +422,18 @@ let get_compiled32 () = let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f -let instantiate21 env l1 = - let rec subst_singleton env t = - CicNotationUtil.group (subst env t) +let add_idrefs = + List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) + +let instantiate21 idrefs env l1 = + let rec subst_singleton env = + function + Ast.AttributedTerm (attr, t) -> + Ast.AttributedTerm (attr, subst_singleton env t) + | t -> CicNotationUtil.group (subst env t) and subst env = function - | Ast.AttributedTerm (attr, t) -> subst env t + | Ast.AttributedTerm (attr, t) as term -> + subst env t | Ast.Variable var -> let name, expected_ty = CicNotationEnv.declaration_of_var var in let ty, value = @@ -438,8 +449,11 @@ let instantiate21 env l1 = assert (CicNotationEnv.well_typed expected_ty value); [ CicNotationEnv.term_of_value value ] | Ast.Magic m -> subst_magic env m - | Ast.Literal (`Keyword k) as t -> [ add_keyword_attrs t ] - | Ast.Literal _ as t -> [ t ] + | Ast.Literal l as t -> + let t = add_idrefs idrefs t in + (match l with + | `Keyword k -> [ add_keyword_attrs t ] + | _ -> [ t ]) | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] and subst_magic env = function @@ -509,19 +523,24 @@ let rec pp_ast1 term = in (* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *) match term with - | Ast.AttributedTerm (attrs, term) -> Ast.AttributedTerm (attrs, pp_ast1 term) + | Ast.AttributedTerm (attrs, term') -> + Ast.AttributedTerm (attrs, pp_ast1 term') | _ -> (match (get_compiled21 ()) term with | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> + | Some (env, ctors, pid) -> + let idrefs = + List.flatten (List.map CicNotationUtil.get_idrefs ctors) + in let prec, assoc, l1 = try Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1)) + add_level_info prec assoc + (instantiate21 idrefs (ast_env_of_env env) l1)) -let instantiate32 term_info env symbol args = +let instantiate32 term_info idrefs env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = (try List.assoc name env with Not_found -> assert false) in @@ -540,28 +559,41 @@ let instantiate32 term_info env symbol args = in add_lambda t (n - count_lambda t) in - let head = Ast.Symbol (symbol, 0) in - match args with - | [] -> head - | _ -> Ast.Appl (head :: List.map instantiate_arg args) + let head = + let symbol = Ast.Symbol (symbol, 0) in + add_idrefs idrefs symbol + in + if args = [] then head + else Ast.Appl (head :: List.map instantiate_arg args) let rec ast_of_acic1 term_info annterm = + let id_to_uris = term_info.uri in + let register_uri id uri = Hashtbl.add id_to_uris id uri in match (get_compiled32 ()) annterm with | None -> ast_of_acic0 term_info annterm ast_of_acic1 - | Some (env, pid) -> + | Some (env, ctors, pid) -> + let idrefs = + List.map + (fun annterm -> + let idref = CicUtil.id_of_annterm annterm in + (try + register_uri idref + (UriManager.string_of_uri + (CicUtil.uri_of_term (Deannotate.deannotate_term annterm))) + with Invalid_argument _ -> ()); + idref) + ctors + in let env' = List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env in - let _, symbol, args, _, uris = + let _, symbol, args, _ = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false in - let ast = instantiate32 term_info env' symbol args in - Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), - (match uris with - | [] -> ast - | _ -> Ast.AttributedTerm (`Href uris, ast))) + let ast = instantiate32 term_info idrefs env' symbol args in + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), ast) let load_patterns32 t = set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) @@ -591,8 +623,7 @@ let fresh_id = let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in - let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in - Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris); + Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern); pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; (try @@ -616,7 +647,7 @@ let lookup_interpretations symbol = (List.sort Pervasives.compare (List.map (fun id -> - let (dsc, _, args, appl_pattern, _) = + let (dsc, _, args, appl_pattern) = try Hashtbl.find level2_patterns32 id with Not_found -> assert false @@ -635,7 +666,7 @@ let add_pretty_printer ~precedence ~associativity l2 l1 = let remove_interpretation id = (try - let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in + let _, symbol, _, _ = Hashtbl.find level2_patterns32 id in let ids = Hashtbl.find interpretations symbol in ids := List.filter ((<>) id) !ids; Hashtbl.remove level2_patterns32 id; diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 651606138..a70b3cbe1 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -29,6 +29,7 @@ val ast_of_acic: Cic.annterm -> (* acic *) CicNotationPt.term (* ast *) * (Cic.id, string) Hashtbl.t (* id -> uri *) + (* TODO change the type of id->uri table to (Cic.id, UriManager.uri) tbl *) (** level 2 -> level 1 *) val pp_ast: CicNotationPt.term -> CicNotationPt.term diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 426846877..966e02626 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -160,6 +160,12 @@ let rec strip_attributes t = in visit_ast ~special_k strip_attributes t +let rec get_idrefs = + function + | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t + | Ast.AttributedTerm (_, t) -> get_idrefs t + | _ -> [] + let meta_names_of_term term = let rec names = ref [] in let add_name n = @@ -297,7 +303,7 @@ let dressn ~sep:sauces = in aux -let find_appl_pattern_uris ap = +(* let find_appl_pattern_uris ap = let rec aux acc = function | Ast.UriPattern uri -> @@ -309,7 +315,7 @@ let find_appl_pattern_uris ap = | Ast.VarPattern _ -> acc | Ast.ApplPattern apl -> List.fold_left aux acc apl in - aux [] ap + aux [] ap *) let rec find_branch = function diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 80e365242..2b035fab7 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -54,6 +54,9 @@ val visit_variable: val strip_attributes: CicNotationPt.term -> CicNotationPt.term + (** @return the list of proper (i.e. non recursive) IdRef of a term *) +val get_idrefs: CicNotationPt.term -> string list + (** generalization of List.combine to n lists *) val ncombine: 'a list list -> 'a list list @@ -66,8 +69,8 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term val group: CicNotationPt.term list -> CicNotationPt.term val ungroup: CicNotationPt.term list -> CicNotationPt.term list -val find_appl_pattern_uris: - CicNotationPt.cic_appl_pattern -> UriManager.uri list +(* val find_appl_pattern_uris: + CicNotationPt.cic_appl_pattern -> UriManager.uri list *) val find_branch: CicNotationPt.term -> CicNotationPt.term diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli index bf4d2cdab..bd7b23adb 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.mli +++ b/helm/ocaml/cic_notation/grafiteAstPp.mli @@ -64,4 +64,5 @@ val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string val pp_dependency: GrafiteAst.dependency -> string - +val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string +