~sep:[space] (List.map (fun x -> [f x]) l)
;;
-let pp_ast0 t k =
+let pp_ast0 status t k =
let rec aux =
function
| Ast.Appl ts ->
in
let match_box =
hvbox false false [
- hvbox false true [
+ hvbox false false [
hvbox false true [keyword "match"; space; break; top_pos (k what)];
break;
hvbox false true indty_box;
keyword "let"; space;
hvbox false true [
aux_var var; space;
- builtin_symbol "\\def"; break; top_pos (k s) ];
- break; space; keyword "in"; space ];
+ builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+ ];
break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
and special_k = function
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
| t ->
- prerr_endline ("unexpected special: " ^ NotationPp.pp_term t);
+ prerr_endline ("unexpected special: " ^ NotationPp.pp_term status t);
assert false
in
aux t
method content_pres_db: db
end
-class status =
+class virtual status =
object
+ inherit NCic.status
val content_pres_db = initial_db
method content_pres_db = content_pres_db
method set_content_pres_db v = {< content_pres_db = v >}
let rec pp_value = function
| NotationEnv.NumValue _ as v -> v
| NotationEnv.StringValue _ as v -> v
-(* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *)
+(* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 status t pp_ast1) *)
| NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 status t)
| NotationEnv.OptValue None as v -> v
| NotationEnv.OptValue (Some v) ->
Ast.AttributedTerm (attrs, pp_ast1 status term')
| _ ->
(match get_compiled21 status term with
- | None -> pp_ast0 term (pp_ast1 status)
+ | None -> pp_ast0 status term (pp_ast1 status)
| Some (env, ctors, pid) ->
let idrefs =
List.flatten (List.map NotationUtil.get_idrefs ctors)
let pp_ast status ast =
debug_print (lazy "pp_ast <-");
let ast' = pp_ast1 status ast in
- debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast'));
+ debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term status ast'));
ast'
let fill_pos_info l1_pattern = l1_pattern
level1_patterns21 =
IntMap.add id l1' status#content_pres_db.level1_patterns21;
pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
- let status = load_patterns21 status status#content_pres_db.pattern21_matrix in
- status,id
+ load_patterns21 status status#content_pres_db.pattern21_matrix
(* presentation -> content *)
in
aux [] env
-let instantiate_level2 env term =
+let instantiate_level2 status env term =
(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
new_name
in
let rec aux env term =
-(* prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
match term with
| Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
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.IdentVar name ->
+ (match Env.lookup_string env name with
+ Env.Ident x -> Ast.Ident (x, None)
+ | Env.Var x -> Ast.Variable (Ast.IdentVar x))
| 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)
| _ ->
prerr_endline (sprintf
"lookup of %s in env %s did not return an optional value"
- name (NotationPp.pp_env env));
+ name (NotationPp.pp_env status env));
assert false))
| Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)