uri: (Cic.id, string) Hashtbl.t;
}
-let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-
let get_types uri =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
| `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 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), List.map k ts)))
+ 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.Box ((Ast.H, false, false), [
- Ast.Literal (`Symbol "\\to"); k body]))])))
+ 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.Layout (Ast.Box ((Ast.HV, false, true), [
- Ast.Layout (Ast.Box ((Ast.H, false, false), [
- Ast.Literal (`Symbol (resolve_binder binder_kind));
- k id;
- Ast.Literal (`Symbol ":");
- aux_ty ty ]));
- Ast.Layout (Ast.Box ((Ast.H, false, false), [
- Ast.Literal (`Symbol ".");
- k body ]))])))
+ binder_symbol (resolve_binder binder_kind);
+ k id;
+ builtin_symbol ":";
+ aux_ty ty;
+ Ast.Layout Ast.Break;
+ builtin_symbol ".";
+ k body ])))
| t -> CicNotationUtil.visit_ast ~special_k k t
and aux_ty = function
- | None -> Ast.Literal (`Symbol "?")
+ | None -> builtin_symbol "?"
| Some ty -> k ty
and special_k = function
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
aux t
let ast_of_acic0 term_info acic k =
-(* prerr_endline "ast_of_acic0"; *)
let k = k term_info in
let register_uri id uri = Hashtbl.add term_info.uri id uri in
let sort_of_id id =
let level1_patterns21 = Hashtbl.create 211
let level2_patterns32 = Hashtbl.create 211
-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 instantiate21 env (* precedence associativity *) l1 =
let rec subst_singleton env t =
- CicNotationUtil.boxify (subst env t)
+ CicNotationUtil.group (subst env t)
and subst env = function
| Ast.AttributedTerm (_, t) -> subst env t
| Ast.Variable var ->
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.Layout l -> [ Ast.Layout (subst_layout env l) ]
| t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
let values = CicNotationUtil.ncombine rec_values in
let sep =
match sep_opt with
- | None -> []
- | Some l -> [ CicNotationPt.Literal l ]
- in
+ | None -> []
+ | Some l -> [ CicNotationPt.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.boxify (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.boxify (subst env p @ sep)) :: acc) tl
+ instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl
in
instantiate_list [] values
| Ast.Opt p ->
end
| _ -> assert false (* impossible *)
and subst_layout env = function
- | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+ | Ast.Box (kind, tl) ->
+ Ast.Box (kind, List.concat (List.map (subst env) tl))
| l -> CicNotationUtil.visit_layout (subst_singleton env) l
in
subst_singleton env l1
let rec pp_value = function
| CicNotationEnv.NumValue _ as v -> v
| CicNotationEnv.StringValue _ as v -> v
+(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
| CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
| CicNotationEnv.OptValue None as v -> v
| CicNotationEnv.OptValue (Some v) ->
let ast_env_of_env env =
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
- 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) (* precedence associativity *) l1))
+ 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
let instantiate32 term_info env symbol args =
let rec instantiate_arg = function
- | Ast.IdentArg (n, name) ->
+ | GrafiteAst.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
let env' =
List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
in
- let symbol, args =
+ let symbol, args, uris =
try
Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
in
- instantiate32 term_info env' symbol args
+ let ast = instantiate32 term_info env' symbol args in
+ match uris with
+ | [] -> ast
+ | _ -> 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
let add_interpretation (symbol, args) appl_pattern =
let id = fresh_id () in
- Hashtbl.add level2_patterns32 id (symbol, args);
+ let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in
+ Hashtbl.add level2_patterns32 id (symbol, args, uris);
pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
load_patterns32 !pattern32_matrix;
id
projects / helm.git / blobdiff