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 xml_of_sort x =
+ let to_string x = Ast.Ident (x, None) in
+ let identify x =
+ add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+ in
+ let lvl t = Ast.AttributedTerm (`Level 90,t) in
+ match x with
+ | `Prop -> identify "Prop"
+ | `Set -> identify "Set"
+ | `CProp _ -> identify "CProp"
+ | `Type _ -> identify "Type"
+ | `NType s -> lvl(Ast.Layout (Ast.Sub (identify "Type",to_string s)))
+ | `NCProp s -> lvl(Ast.Layout (Ast.Sub (identify "CProp",to_string s)))
+;;
+
+
+let map_space f l =
+ HExtlib.list_concat
+ ~sep:[space] (List.map (fun x -> [f x]) l)
+;;
let pp_ast0 t k =
let rec aux =
let mk_case_pattern =
function
Ast.Pattern (head, href, vars) ->
- hbox true false (ident_w_href href head :: List.map aux_var vars)
+ hvbox true true (ident_w_href href head ::
+ List.flatten (List.map (fun x -> [break;x]) (map_space aux_var vars)))
| Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
List.map
(fun (lhs, rhs) ->
remove_level_info
- (hvbox false true [
- hbox false true [
- mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ];
+ (hovbox false true [
+ mk_case_pattern lhs; break; builtin_symbol "\\Rightarrow";
break; top_pos (k rhs) ]))
patterns
in
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
in
let mk_fun (args, (name,ty), body, rec_param) =
- List.map aux_var args ,k name, HExtlib.map_option k ty, k body,
- fst (List.nth args rec_param)
+ List.flatten (List.map (fun x -> [aux_var x; space]) args),
+ k name, HExtlib.map_option k ty, k body, fst (List.nth args rec_param)
in
let mk_funs = List.map mk_fun in
let fst_fun, tl_funs =
space;
keyword rec_op;
space;
- name] @
+ name;
+ space] @
params @
- [space; keyword "on" ; space ; rec_param ;space ] @
+ [keyword "on" ; space ; rec_param ;space ] @
(match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
[ builtin_symbol "\\def";
break;
(fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
- keyword "and";
+ keyword "and"; space;
name] @
params @
[space; keyword "on" ; space; rec_param ;space ] @
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
- | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Implicit `JustOne -> builtin_symbol "?"
+ | Ast.Implicit `Vector -> builtin_symbol "…"
| Ast.Meta (n, l) ->
let local_context l =
List.map (function None -> None | Some t -> Some (k t)) l
| 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_sort sort_kind = xml_of_sort sort_kind
and aux_ty = function
| None -> builtin_symbol "?"
| Some ty -> k ty
(* persistent state *)
-let level1_patterns21 = Hashtbl.create 211
-
+let initial_level1_patterns21 () = Hashtbl.create 211
+let level1_patterns21 = ref (initial_level1_patterns21 ())
let compiled21 = ref None
-
let pattern21_matrix = ref []
+let counter = ref ~-1
+
+let stack = ref [];;
+
+let push () =
+ stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack;
+ counter := ~-1;
+ level1_patterns21 := initial_level1_patterns21 ();
+ compiled21 := None;
+ pattern21_matrix := []
+;;
+
+let pop () =
+ match !stack with
+ [] -> assert false
+ | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old ->
+ stack := old;
+ counter := ocounter;
+ level1_patterns21 := olevel1_patterns21;
+ compiled21 := ocompiled21;
+ pattern21_matrix := opatterns21_matrix
+;;
let get_compiled21 () =
match !compiled21 with
assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
- assert (CicNotationEnv.well_typed expected_ty value);
+ if not (CicNotationEnv.well_typed expected_ty value) then
+ begin
+ prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration");
+ assert false
+ end;
let value = CicNotationEnv.term_of_value value in
let value =
match expected_ty with
let terms = subst pos env p in
instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
- [hovbox false false (instantiate_list [] values)]
+ if values = [] then []
+ else [hovbox false false (instantiate_list [] values)]
| Ast.Opt p ->
let opt_decls = CicNotationEnv.declarations_of_term p in
let env =
in
let l1 =
try
- Hashtbl.find level1_patterns21 pid
+ Hashtbl.find !level1_patterns21 pid
with Not_found -> assert false
in
instantiate21 idrefs (ast_env_of_env env) l1)
in
aux true l1_pattern *)
-let counter = ref ~-1
-let reset () =
- counter := ~-1;
- Hashtbl.clear level1_patterns21
-;;
let fresh_id =
fun () ->
incr counter;
let id = fresh_id () in
let l1' = add_level_info precedence (fill_pos_info l1) in
let l2' = CicNotationUtil.strip_attributes l2 in
- Hashtbl.add level1_patterns21 id l1';
+ Hashtbl.add !level1_patterns21 id l1';
pattern21_matrix := (l2', id) :: !pattern21_matrix;
load_patterns21 !pattern21_matrix;
id
let remove_pretty_printer id =
(try
- Hashtbl.remove level1_patterns21 id;
+ Hashtbl.remove !level1_patterns21 id;
with Not_found -> raise Pretty_printer_not_found);
pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
load_patterns21 !pattern21_matrix
aux ((name, (ty, v)) :: acc) tl
| Env.TermType _, Env.TermValue _ ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType _, Env.OptValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
| Env.TermType _, Env.TermValue _ ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType _, Env.OptValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| binding :: tl -> aux (binding :: acc) tl
| [] -> acc
Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
| Ast.Magic magic -> aux_magic env magic
| Ast.Variable var -> aux_variable env var
+ | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
+
| _ -> assert false
and aux_opt env = function
| Some term -> Some (aux env term)
projects / helm.git / blobdiff