type interpretation_id = pattern_id
type pretty_printer_id = pattern_id
-let default_prec = 50
-let default_assoc = Gramext.NonA
+module Ast = CicNotationPt
type term_info =
- { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
+ { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
uri: (Cic.id, string) Hashtbl.t;
}
fst (List.nth (constructors_of_inductive_type uri i) (j-1))
with Not_found -> assert false)
-module Ast = CicNotationPt
-module Parser = CicNotationParser
-
-let string_of_name = function
- | Cic.Name s -> s
- | Cic.Anonymous -> "_"
-
-let ident_of_name n = Ast.Ident (string_of_name n, None)
-
let idref id t = Ast.AttributedTerm (`IdRef id, t)
let resolve_binder = function
in
let rec aux = function
| Ast.Appl ts ->
- Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+ Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc),
Ast.Layout
(Ast.Box ((Ast.HOV, true, true),
(CicNotationUtil.dress
(List.map k ts)))))
| Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
| Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
- Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+ Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
aux_ty ty;
Ast.Layout Ast.Break;
binder_symbol "\\to";
k body])))
| Ast.Binder (binder_kind, (id, ty), body) ->
- Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+ Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc),
Ast.Layout (Ast.Box ((Ast.HV, false, true), [
binder_symbol (resolve_binder binder_kind);
k id;
| `Set | `Type -> `Pi
| `Prop | `CProp -> `Forall
in
- idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t))
- | Cic.ACast (id,v,t) ->
- idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t])
+ idref id (Ast.Binder (binder_kind,
+ (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
+ | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t))
| Cic.ALambda (id,n,s,t) ->
- idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t))
+ idref id (Ast.Binder (`Lambda,
+ (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))
| Cic.ALetIn (id,n,s,t) ->
- idref id (Ast.LetIn ((ident_of_name n, None), k s, k t))
+ idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
+ k s, k t))
| Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
| Cic.AConst (id,uri,substs) ->
register_uri id (UriManager.string_of_uri uri);
match (ty, pat) with
| Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') ->
let (cv, rhs) = eat_branch t t' in
- (ident_of_name name, Some (k s)) :: cv, rhs
+ (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs
| _, _ -> [], k pat
in
let patterns =
let level1_patterns21 = Hashtbl.create 211
let level2_patterns32 = Hashtbl.create 211
+let interpretations = Hashtbl.create 211 (* symb -> id list ref *)
-let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option)
-option ref) =
- ref None
-let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option)
-option ref) =
- ref None
+let compiled21 = ref None
+let compiled32 = ref None
let pattern21_matrix = ref []
let pattern32_matrix = ref []
let get_compiled21 () =
match !compiled21 with
| None -> assert false
- | Some f -> f
+ | Some f -> Lazy.force f
let get_compiled32 () =
match !compiled32 with
| None -> assert false
- | Some f -> f
+ | Some f -> Lazy.force f
let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
let sep =
match sep_opt with
| None -> []
- | Some l -> [ CicNotationPt.Literal l ]
+ | Some l -> [ Ast.Literal l ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
let env' =
List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
in
- let symbol, args, uris =
+ let _, symbol, args, _, uris =
try
Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
| _ -> Ast.AttributedTerm (`Href uris, ast)
let load_patterns32 t =
- set_compiled32 (CicNotationMatcher.Matcher32.compiler t)
+ set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
let load_patterns21 t =
- set_compiled21 (CicNotationMatcher.Matcher21.compiler t)
+ set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t))
let ast_of_acic id_to_sort annterm =
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
incr counter;
!counter
-let add_interpretation (symbol, args) appl_pattern =
+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 (symbol, args, uris);
+ Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris);
pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
load_patterns32 !pattern32_matrix;
+ (try
+ let ids = Hashtbl.find interpretations symbol in
+ ids := id :: !ids
+ with Not_found -> Hashtbl.add interpretations symbol (ref [id]));
id
-let add_pretty_printer
- ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
-=
+exception Interpretation_not_found
+exception Pretty_printer_not_found
+
+let lookup_interpretations symbol =
+ try
+ List.map
+ (fun id ->
+ let (dsc, _, args, appl_pattern, _) =
+ try
+ Hashtbl.find level2_patterns32 id
+ with Not_found -> assert false
+ in
+ dsc, args, appl_pattern)
+ !(Hashtbl.find interpretations symbol)
+ with Not_found -> raise Interpretation_not_found
+
+let add_pretty_printer ~precedence ~associativity l2 l1 =
let id = fresh_id () in
let l2' = CicNotationUtil.strip_attributes l2 in
Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
load_patterns21 !pattern21_matrix;
id
-exception Interpretation_not_found
-exception Pretty_printer_not_found
-
let remove_interpretation id =
(try
+ 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;
with Not_found -> raise Interpretation_not_found);
pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;