open Printf
-module Ast = CicNotationPt
-module Env = CicNotationEnv
+module Ast = NotationPt
+module Env = NotationEnv
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
-let rec top_pos t = add_level_info ~-1 t
+let top_pos t = add_level_info ~-1 t
let rec remove_level_info =
function
match href with
| None -> ident i
| Some href ->
- let href = UriManager.string_of_uri href in
+ let href = NReference.string_of_reference href in
add_xml_attrs [Some "xlink", "href", href] (ident i)
let binder_symbol s =
~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 ->
(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 70 ts)))
+ (hovbox true true (NotationUtil.dress break (aux_args 70 ts)))
| Ast.Binder (binder_kind, (id, ty), body) ->
add_level_info Ast.binder_prec
(hvbox false true
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) ->
let rec_op =
match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
+*)
| Ast.Implicit `JustOne -> builtin_symbol "?"
| Ast.Implicit `Vector -> builtin_symbol "…"
| Ast.Meta (n, l) ->
| Ast.Uri (_, None) | Ast.Uri (_, Some [])
| Ast.Literal _
| Ast.UserInput as leaf -> leaf
- | t -> CicNotationUtil.visit_ast ~special_k k t
+ | t -> NotationUtil.visit_ast ~special_k k t
and aux_sort sort_kind = xml_of_sort sort_kind
and aux_ty = function
| None -> builtin_symbol "?"
and special_k = function
| Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
| t ->
- prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t);
+ prerr_endline ("unexpected special: " ^ NotationPp.pp_term status t);
assert false
in
aux t
(* persistent state *)
-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
- | None -> assert false
- | Some f -> Lazy.force f
-
-let set_compiled21 f = compiled21 := Some f
+module IntMap = Map.Make(struct type t = int let compare = compare end);;
+
+type db = {
+ level1_patterns21: NotationPt.term IntMap.t;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
+ pattern21_matrix: (NotationPt.term * pattern_id) list;
+ counter: pattern_id
+}
+
+let initial_db = {
+ level1_patterns21 = IntMap.empty;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
+ pattern21_matrix = [];
+ counter = ~-1
+}
+
+class type g_status =
+ object
+ method content_pres_db: db
+ end
+
+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 >}
+ method set_content_pres_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< content_pres_db = o#content_pres_db >}
+ end
+
+let get_compiled21 status =
+ Lazy.force status#content_pres_db.compiled21
+
+let set_compiled21 status f =
+ status#set_content_pres_db
+ { status#content_pres_db with compiled21 = f }
let add_idrefs =
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
function
Ast.AttributedTerm (attr, t) ->
Ast.AttributedTerm (attr, subst_singleton pos env t)
- | t -> CicNotationUtil.group (subst pos env t)
+ | t -> NotationUtil.group (subst pos env t)
and subst pos env = function
- | Ast.AttributedTerm (attr, t) ->
-(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
+ | Ast.AttributedTerm (_attr, t) ->
+(* prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *)
subst pos env t
| Ast.Variable var ->
- let name, expected_ty = CicNotationEnv.declaration_of_var var in
+ let name, expected_ty = NotationEnv.declaration_of_var var in
let ty, value =
try
List.assoc name env
prerr_endline ("name " ^ name ^ " not found in environment");
assert false
in
- assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
+ assert (NotationEnv.well_typed ty value); (* INVARIANT *)
(* following assertion should be a conditional that makes this
* instantiation fail *)
- if not (CicNotationEnv.well_typed expected_ty value) then
+ if not (NotationEnv.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 = NotationEnv.term_of_value value in
let value =
match expected_ty with
| Env.TermType l -> Ast.AttributedTerm (`Level l,value)
| Ast.Literal l as t ->
let t = add_idrefs idrefs t in
(match l with
- | `Keyword k -> [ add_keyword_attrs t ]
+ | `Keyword _k -> [ add_keyword_attrs t ]
| _ -> [ t ])
| Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
- | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ]
+ | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
- let rec_decls = CicNotationEnv.declarations_of_term p in
+ let rec_decls = NotationEnv.declarations_of_term p in
let rec_values =
- List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
+ List.map (fun (n, _) -> NotationEnv.lookup_list env n) rec_decls
in
- let values = CicNotationUtil.ncombine rec_values in
+ let values = NotationUtil.ncombine rec_values in
let sep =
match sep_opt with
| None -> []
let rec instantiate_list acc = function
| [] -> List.rev acc
| value_set :: [] ->
- let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list (CicNotationUtil.group (subst pos env p) :: acc)
+ let env = NotationEnv.combine rec_decls value_set in
+ instantiate_list (NotationUtil.group (subst pos env p) :: acc)
[]
| value_set :: tl ->
- let env = CicNotationEnv.combine rec_decls value_set in
+ let env = NotationEnv.combine rec_decls value_set in
let terms = subst pos env p in
- instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
+ instantiate_list (NotationUtil.group (terms @ sep) :: acc) tl
in
if values = [] then []
else [hovbox false false (instantiate_list [] values)]
| Ast.Opt p ->
- let opt_decls = CicNotationEnv.declarations_of_term p in
+ let opt_decls = NotationEnv.declarations_of_term p in
let env =
let rec build_env = function
| [] -> []
| (name, ty) :: tl ->
(* assumption: if one of the value is None then all are *)
- (match CicNotationEnv.lookup_opt env name with
+ (match NotationEnv.lookup_opt env name with
| None -> raise Exit
| Some v -> (name, (ty, v)) :: build_env tl)
in
| Ast.Box (kind, tl) ->
let tl' = subst_children pos env tl in
Ast.Box (kind, List.concat tl')
- | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
+ | l -> NotationUtil.visit_layout (subst_singleton pos env) l
and subst_children pos env =
function
| [] -> []
in
subst_singleton `Left env l1
-let rec pp_ast1 term =
+let rec pp_ast1 status term =
let rec pp_value = function
- | CicNotationEnv.NumValue _ as v -> v
- | CicNotationEnv.StringValue _ as v -> v
-(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
- | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
- | CicNotationEnv.OptValue None as v -> v
- | CicNotationEnv.OptValue (Some v) ->
- CicNotationEnv.OptValue (Some (pp_value v))
- | CicNotationEnv.ListValue vl ->
- CicNotationEnv.ListValue (List.map pp_value vl)
+ | NotationEnv.NumValue _ as v -> v
+ | NotationEnv.StringValue _ as v -> v
+(* | 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) ->
+ NotationEnv.OptValue (Some (pp_value v))
+ | NotationEnv.ListValue vl ->
+ NotationEnv.ListValue (List.map pp_value vl)
in
let ast_env_of_env env =
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
-(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
+(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *)
match term with
| Ast.AttributedTerm (attrs, term') ->
- Ast.AttributedTerm (attrs, pp_ast1 term')
+ Ast.AttributedTerm (attrs, pp_ast1 status term')
| _ ->
- (match (get_compiled21 ()) term with
- | None -> pp_ast0 term pp_ast1
+ (match get_compiled21 status term with
+ | None -> pp_ast0 status term (pp_ast1 status)
| Some (env, ctors, pid) ->
let idrefs =
- List.flatten (List.map CicNotationUtil.get_idrefs ctors)
+ List.flatten (List.map NotationUtil.get_idrefs ctors)
in
let l1 =
try
- Hashtbl.find !level1_patterns21 pid
+ IntMap.find pid status#content_pres_db.level1_patterns21
with Not_found -> assert false
in
instantiate21 idrefs (ast_env_of_env env) l1)
-let load_patterns21 t =
- set_compiled21 (lazy (Content2presMatcher.Matcher21.compiler t))
+let load_patterns21 status t =
+ set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))
-let pp_ast ast =
+let pp_ast status ast =
debug_print (lazy "pp_ast <-");
- let ast' = pp_ast1 ast in
- debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast'));
+ let ast' = pp_ast1 status ast in
+ debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term status ast'));
ast'
-exception Pretty_printer_not_found
-
let fill_pos_info l1_pattern = l1_pattern
(* let rec aux toplevel pos =
function
in
aux true l1_pattern *)
-let fresh_id =
- fun () ->
- incr counter;
- !counter
+let fresh_id status =
+ let counter = status#content_pres_db.counter+1 in
+ status#set_content_pres_db ({ status#content_pres_db with counter = counter }), counter
-let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
- let id = fresh_id () in
+let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) =
+ let status,id = fresh_id status 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';
- pattern21_matrix := (l2', id) :: !pattern21_matrix;
- load_patterns21 !pattern21_matrix;
- id
-
-let remove_pretty_printer id =
- (try
- 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
+ let l2' = NotationUtil.strip_attributes l2 in
+ let status =
+ status#set_content_pres_db
+ { status#content_pres_db with
+ level1_patterns21 =
+ IntMap.add id l1' status#content_pres_db.level1_patterns21;
+ pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
+ load_patterns21 status status#content_pres_db.pattern21_matrix
(* presentation -> content *)
in
aux [] env
-let instantiate_level2 env term =
-(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *)
+let instantiate_level2 status env term =
+(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
try
List.assoc n !fresh_env
with Not_found ->
- let new_name = CicNotationUtil.fresh_name () in
+ let new_name = NotationUtil.fresh_name () in
fresh_env := (n, new_name) :: !fresh_env;
new_name
in
let rec aux env term =
-(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
match term with
- | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)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)
List.map (aux_branch env) patterns)
| Ast.LetIn (var, t1, t3) ->
Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
+(*
| Ast.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
+*)
| Ast.Uri (name, None) -> Ast.Uri (name, None)
| Ast.Uri (name, Some substs) ->
Ast.Uri (name, Some (aux_substs env substs))
Ast.Pattern (head, hrefs, vars) ->
Ast.Pattern (head, hrefs, List.map (aux_capture_var env) vars)
| Ast.Wildcard -> Ast.Wildcard
- and aux_definition env (params, var, term, i) =
- (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
+ (*and aux_definition env (params, var, term, i) =
+ (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)*)
and aux_substs env substs =
List.map (fun (name, term) -> (name, aux env term)) substs
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)
- | Ast.Ascription (term, name) -> assert false
+ | Ast.Ascription (_term, _name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
- let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
- let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
+ let some_pattern_names = NotationUtil.names_of_term some_pattern in
+ let none_pattern_names = NotationUtil.names_of_term none_pattern in
let opt_names =
List.filter
(fun name -> not (List.mem name none_pattern_names))
| _ ->
prerr_endline (sprintf
"lookup of %s in env %s did not return an optional value"
- name (CicNotationPp.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 *)
let meta_names =
List.filter ((<>) acc_name)
- (CicNotationUtil.names_of_term rec_pattern)
+ (NotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
List.filter ((<>) acc_name)
- (CicNotationUtil.names_of_term rec_pattern)
+ (NotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
| _ -> assert false
in
instantiate_fold_right env)
- | Ast.If (_, p_true, p_false) as t ->
- aux env (CicNotationUtil.find_branch (Ast.Magic t))
+ | Ast.If (_, _p_true, _p_false) as t ->
+ aux env (NotationUtil.find_branch (Ast.Magic t))
| Ast.Fail -> assert false
| _ -> assert false
in
aux env term
-
- (* initialization *)
-
-let _ = load_patterns21 []
-
-
-
projects / helm.git / blobdiff