| 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;
projects / helm.git / blobdiff