now kept at the Ast level.
Still issues in idref propagation for magics.
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) =
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
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 =
| _ -> 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)
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 =
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
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 ->
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
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
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
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
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 <pattern, pattern_id>)
+ * @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
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
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 =
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
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
| `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
| `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
| `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
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
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 *)
| 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)
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)
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
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 =
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
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
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))
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
(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
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;
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
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 =
in
aux
-let find_appl_pattern_uris ap =
+(* let find_appl_pattern_uris ap =
let rec aux acc =
function
| Ast.UriPattern uri ->
| Ast.VarPattern _ -> acc
| Ast.ApplPattern apl -> List.fold_left aux acc apl
in
- aux [] ap
+ aux [] ap *)
let rec find_branch =
function
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
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
val pp_dependency: GrafiteAst.dependency -> string
-
+val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string
+
projects / helm.git / commitdiff