| `Set -> "Set"
| `CProp _ -> "CProp"
| `Type _ -> "Type"
+ | `NType s -> "Type[" ^ s ^ "]"
let pp_ast0 t k =
let rec aux =
(* 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
and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
- prerr_endline "1";
let rec_decls = CicNotationEnv.declarations_of_term p in
- prerr_endline "2";
let rec_values =
List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
in
- prerr_endline "3";
let values = CicNotationUtil.ncombine rec_values in
- prerr_endline "4";
let sep =
match sep_opt with
| None -> []
| Some l -> [ Ast.Literal l; break; space ]
in
- prerr_endline "5";
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->
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
| 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)