| `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 (Ast.apply_prec, Ast.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 (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])))
+ 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 (Ast.binder_prec, Ast.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
| 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 =
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
| [] -> 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
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 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
projects / helm.git / blobdiff