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
| `Forall -> "\\forall"
| `Exists -> "\\exists"
-let binder_attributes = [None, "mathcolor", "blue"]
-let atop_attributes = [None, "linethickness", "0pt"]
-let indent_attributes = [None, "indent", "1em"]
-let keyword_attributes = [None, "mathcolor", "blue"]
+let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t)
+
+let rec remove_level_info =
+ function
+ | Ast.AttributedTerm (`Level _, t) -> remove_level_info t
+ | 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_keyword_attrs =
+ add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+let box kind spacing indent content =
+ Ast.Layout (Ast.Box ((kind, spacing, indent), content))
+let hbox = box Ast.H
+let vbox = box Ast.V
+let hvbox = box Ast.HV
+let hovbox = box Ast.HOV
+let break = Ast.Layout Ast.Break
+let reset_href t = Ast.AttributedTerm (`Href [], t)
+let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
+let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
+let number s =
+ reset_href
+ (add_xml_attrs (RenderingAttrs.number_attributes `MathML)
+ (Ast.Literal (`Number s)))
+let ident i =
+ add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+let binder_symbol s =
+ add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
+ (builtin_symbol s)
+
+let string_of_sort_kind = function
+ | `Prop -> "Prop"
+ | `Set -> "Set"
+ | `CProp -> "CProp"
+ | `Type -> "Type"
let pp_ast0 t k =
- let reset_href t = Ast.AttributedTerm (`Href [], t) in
- let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
- let binder_symbol s =
- Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s)
- in
let rec aux = function
| Ast.Appl ts ->
- Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
- Ast.Layout
- (Ast.Box ((Ast.HOV, true, true),
- (CicNotationUtil.dress
- (Ast.Layout Ast.Break)
- (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.Layout (Ast.Box ((Ast.HV, false, true), [
- aux_ty ty;
- Ast.Layout Ast.Break;
- binder_symbol "\\to";
- k body])))
+ add_level_info Ast.apply_prec Ast.apply_assoc
+ (hovbox true true (CicNotationUtil.dress break (List.map k ts)))
| Ast.Binder (binder_kind, (id, ty), body) ->
- Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
- Ast.Layout (Ast.Box ((Ast.HV, false, true), [
- binder_symbol (resolve_binder binder_kind);
- k id;
- builtin_symbol ":";
- aux_ty ty;
- Ast.Layout Ast.Break;
- builtin_symbol ".";
- k body ])))
+ add_level_info Ast.binder_prec Ast.binder_assoc
+ (hvbox false true
+ [ binder_symbol (resolve_binder binder_kind);
+ k id; builtin_symbol ":"; aux_ty ty; break;
+ builtin_symbol "."; k body ])
+ | Ast.Case (what, indty_opt, outty_opt, patterns) ->
+ let outty_box =
+ match outty_opt with
+ | None -> []
+ | Some outty ->
+ [ builtin_symbol "["; remove_level_info (k outty);
+ builtin_symbol "]"; break ]
+ in
+ let indty_box =
+ match indty_opt with
+ | None -> []
+ | Some indty -> [ keyword "in"; ident indty ]
+ in
+ let match_box =
+ hvbox false true [
+ keyword "match"; break;
+ hvbox false false ([ k what ] @ indty_box); break;
+ keyword "with" ]
+ in
+ let mk_case_pattern (head, vars) =
+ hbox true false (ident head :: List.map aux_var vars)
+ in
+ let patterns' =
+ List.map
+ (fun (lhs, rhs) ->
+ remove_level_info
+ (hvbox false true [
+ hbox false true [
+ mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ];
+ break; k rhs ]))
+ patterns
+ in
+ let patterns'' =
+ let rec aux_patterns = function
+ | [] -> assert false
+ | [ last ] ->
+ [ break;
+ hbox false false [
+ builtin_symbol "|";
+ last; builtin_symbol "]" ] ]
+ | hd :: tl ->
+ [ break; hbox false false [ builtin_symbol "|"; hd ] ]
+ @ aux_patterns tl
+ in
+ match patterns' with
+ | [] ->
+ [ hbox false false [ builtin_symbol "["; builtin_symbol "]" ] ]
+ | [ one ] ->
+ [ hbox false false [
+ builtin_symbol "["; one; builtin_symbol "]" ] ]
+ | hd :: tl ->
+ hbox false false [ builtin_symbol "["; hd ]
+ :: aux_patterns tl
+ in
+ add_level_info Ast.simple_prec Ast.simple_assoc
+ (hvbox false false [
+ hvbox false false (outty_box @ [ match_box ]); break;
+ hbox false false [ hvbox false false patterns'' ] ])
+ | Ast.Cast (bo, ty) ->
+ add_level_info Ast.simple_prec Ast.simple_assoc
+ (hvbox false true [
+ builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty;
+ builtin_symbol ")"])
+ | Ast.LetIn (var, s, t) ->
+ add_level_info Ast.let_in_prec Ast.let_in_assoc
+ (hvbox false true [
+ hvbox false true [
+ keyword "let";
+ hvbox false true [
+ aux_var var; builtin_symbol "\\def"; break; k s ];
+ break; keyword "in" ];
+ k t ])
+ | Ast.LetRec (rec_kind, funs, where) ->
+ let rec_op =
+ match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
+ in
+ let mk_fun (var, body, _) = aux_var var, k body in
+ let mk_funs = List.map mk_fun in
+ let fst_fun, tl_funs =
+ match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false
+ in
+ let fst_row =
+ let (name, body) = fst_fun in
+ hvbox false true [
+ keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break;
+ body ]
+ in
+ let tl_rows =
+ List.map
+ (fun (name, body) ->
+ [ break;
+ hvbox false true [
+ keyword "and"; name; builtin_symbol "\\def"; break; body ] ])
+ tl_funs
+ in
+ add_level_info Ast.let_in_prec Ast.let_in_assoc
+ ((hvbox false false
+ (fst_row :: List.flatten tl_rows
+ @ [ break; keyword "in"; break; k where ])))
+ | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Meta (n, l) ->
+ let local_context l =
+ CicNotationUtil.dress (builtin_symbol ";")
+ (List.map (function None -> builtin_symbol "_" | Some t -> k t) l)
+ in
+ hbox false false
+ ([ builtin_symbol "?"; number (string_of_int n) ]
+ @ (if l <> [] then local_context l else []))
+ | Ast.Sort sort -> aux_sort sort
+ | Ast.Num _
+ | Ast.Symbol _
+ | Ast.Ident (_, None) | Ast.Ident (_, Some [])
+ | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+ | Ast.Literal _
+ | Ast.UserInput as leaf -> leaf
| t -> CicNotationUtil.visit_ast ~special_k k t
+ and aux_sort sort_kind =
+ add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+ (Ast.Ident (string_of_sort_kind sort_kind, None))
and aux_ty = function
| None -> builtin_symbol "?"
| Some ty -> k ty
+ and aux_var = function
+ | name, Some ty ->
+ hvbox false true [
+ builtin_symbol "("; name; builtin_symbol ":"; break; k ty;
+ builtin_symbol ")" ]
+ | name, None -> name
and special_k = function
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
- | _ -> assert false
+ | t ->
+ prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t);
+ assert false
in
aux t
let sort_of_id id =
try
Hashtbl.find term_info.sort id
- with Not_found -> assert false
+ with Not_found ->
+ prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
+ `Type
in
let aux_substs substs =
Some
| `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 =
| Cic.ACoFix (id, no, funs) ->
let defs =
List.map
- (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
+ (fun (_, n, ty, bo) ->
+ ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
funs
in
let name =
let level1_patterns21 = Hashtbl.create 211
let level2_patterns32 = Hashtbl.create 211
+let interpretations = Hashtbl.create 211 (* symb -> id list ref *)
let compiled21 = ref None
let compiled32 = ref None
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 ->
- [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ]
- | Ast.Literal _ as t -> [ t ]
+ | Ast.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ]
+ | Ast.Literal _ as t -> [ (*reset_href*) t ]
| Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
| t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
and subst_magic env = function
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
| value_set :: [] ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
+ instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
+ instantiate_list
+ (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
in
instantiate_list [] values
| Ast.Opt p ->
match term with
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
| _ ->
- begin
- match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
- | Some (env, pid) ->
- let precedence, associativity, l1 =
- try
- Hashtbl.find level1_patterns21 pid
- with Not_found -> assert false
- in
- Ast.AttributedTerm (`Level (precedence, associativity),
- (instantiate21 (ast_env_of_env env) l1))
- end
+ (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))
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
- | GrafiteAst.IdentArg (n, name) ->
+ | Ast.IdentArg (n, name) ->
let t = (try List.assoc name env with Not_found -> assert false) in
let rec count_lambda = function
| Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
in
add_lambda t (n - count_lambda t)
in
- let args' = List.map instantiate_arg args in
- Ast.Appl (Ast.Symbol (symbol, 0) :: args')
+ let head = Ast.Symbol (symbol, 0) in
+ match args with
+ | [] -> head
+ | _ -> Ast.Appl (head :: List.map instantiate_arg args)
let rec ast_of_acic1 term_info annterm =
match (get_compiled32 ()) annterm with
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
in
let ast = instantiate32 term_info env' symbol args in
- match uris with
- | [] -> ast
- | _ -> Ast.AttributedTerm (`Href uris, ast)
+ Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm),
+ (match uris with
+ | [] -> ast
+ | _ -> Ast.AttributedTerm (`Href uris, ast)))
let load_patterns32 t =
set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
let ast = ast_of_acic1 term_info annterm in
ast, term_info.uri
-let pp_ast term = pp_ast1 term
+let pp_ast term =
+(* prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *)
+ pp_ast1 term
let fresh_id =
let counter = ref ~-1 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 rec list_uniq = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
+
+let lookup_interpretations symbol =
+ try
+ list_uniq
+ (List.sort Pervasives.compare
+ (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;
projects / helm.git / blobdiff