| `Set -> "Set"
| `CProp _ -> "CProp"
| `Type _ -> "Type"
+ | `NType s -> "Type[" ^ s ^ "]"
let pp_ast0 t k =
let rec aux =
function
| Ast.Appl ts ->
- let rec aux_args pos =
+ let rec aux_args level =
function
| [] -> []
| [ last ] ->
- let last = k last in
- [ last ]
+ [ Ast.AttributedTerm (`Level level,k last) ]
| hd :: tl ->
- (k hd) :: aux_args `Inner tl
+ (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
in
add_level_info Ast.apply_prec
- (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
+ (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
| Ast.Binder (binder_kind, (id, ty), body) ->
add_level_info Ast.binder_prec
(hvbox false true
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 false (ident_w_href href head :: List.map aux_var vars)
| Ast.Wildcard -> builtin_symbol "_"
in
let patterns' =
hvbox false true [
aux_var var; space;
builtin_symbol "\\def"; break; top_pos (k s) ];
- break; space; keyword "in" ];
+ break; space; keyword "in"; space ];
break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
(* 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
- | Env.TermType (Some l) ->
- Ast.AttributedTerm (`Level l,value)
+ | Env.TermType l -> Ast.AttributedTerm (`Level l,value)
| _ -> value
in
[ value ]
let sep =
match sep_opt with
| None -> []
- | Some l -> [ Ast.Literal l ]
+ | Some l -> [ Ast.Literal l; break; space ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
let terms = subst pos env p in
instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
- 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
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.TermType _, Env.TermValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
(match ty, v with
| Env.ListType ty, Env.ListValue (_ :: vtl) ->
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
+ | Env.TermType _, Env.TermValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| binding :: tl -> aux (binding :: acc) tl
| [] -> acc
aux [] env
let instantiate_level2 env term =
+(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
try
let rec aux env term =
(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
match term with
- | Ast.AttributedTerm (_, term) -> aux env term
+ | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
| Ast.Binder (binder, var, body) ->
Ast.Binder (binder, aux_capture_var env var, aux env body)
| 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)
and aux_variable env = function
| Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
| Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
- | Ast.TermVar (name,None) ->
- Env.lookup_term env name
- | Ast.TermVar (name,Some l) ->
+ | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) ->
Ast.AttributedTerm (`Level l,Env.lookup_term env name)
| Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
| Ast.Ascription (term, name) -> assert false
| Env.ListValue (_ :: _) ->
instantiate_fold_left
(let acc_binding =
- acc_name, (Env.TermType None, Env.TermValue acc)
+ acc_name, (Env.TermType 0, Env.TermValue acc)
in
aux (acc_binding :: head_names names env') rec_pattern)
(tail_names names env')
| Env.ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
let acc_binding =
- acc_name, (Env.TermType None, Env.TermValue acc)
+ acc_name, (Env.TermType 0, Env.TermValue acc)
in
aux (acc_binding :: head_names names env') rec_pattern
| Env.ListValue [] -> aux env base_pattern
projects / helm.git / blobdiff