module Ast = CicNotationPt
let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
type pattern_id = int
type interpretation_id = pattern_id
| 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)
| `Prop -> "Prop"
| `Set -> "Set"
| `CProp -> "CProp"
- | `Type -> "Type"
+ | `Type _ -> "Type"
let pp_ast0 t k =
let rec aux =
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
with Not_found ->
prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
- `Type
+ `Type (CicUniv.fresh ())
in
let aux_substs substs =
Some
| Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
| Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
| Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
- | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
+ | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
| Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
| Cic.AImplicit _ -> assert false
| Cic.AProd (id,n,s,t) ->
let binder_kind =
match sort_of_id id with
- | `Set | `Type -> `Pi
+ | `Set | `Type _ -> `Pi
| `Prop | `CProp -> `Forall
in
idref id (Ast.Binder (binder_kind,
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
-let instantiate21 env (* precedence associativity *) 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 (_, 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
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
- 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))
+ match term with
+ | Ast.AttributedTerm (attrs, term') ->
+ Ast.AttributedTerm (attrs, pp_ast1 term')
+ | _ ->
+ (match (get_compiled21 ()) term with
+ | None -> pp_ast0 term pp_ast1
+ | 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 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))
set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
let ast_of_acic id_to_sort annterm =
- debug_print ("ast_of_acic <- "
- ^ CicPp.ppterm (Deannotate.deannotate_term annterm));
+ debug_print (lazy ("ast_of_acic <- "
+ ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast = ast_of_acic1 term_info annterm in
- debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast);
+ debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
ast, term_info.uri
let pp_ast ast =
- debug_print "pp_ast <-";
+ debug_print (lazy "pp_ast <-");
let ast' = pp_ast1 ast in
- debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast');
+ debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
ast'
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
(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