type pattern_id = int
type interpretation_id = pattern_id
+type pretty_printer_id = pattern_id
type term_info =
{ sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-module Patterns =
+module type PATTERN =
+ sig
+ type pattern_t
+ val compatible : pattern_t -> pattern_t -> bool
+ end
+
+module Patterns (P: PATTERN) =
struct
- type row_t = CicNotationPt.cic_appl_pattern list * pattern_id
+ type row_t = P.pattern_t list * pattern_id
type t = row_t list
let empty = []
let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t
let pattern_ids t = List.map snd t
- let prepend_column t column =
- try
- List.map2 (fun elt (pl, pid) -> (elt :: pl), pid) column t
+ let partition t pidl =
+ let partitions = Hashtbl.create 11 in
+ let add pid row = Hashtbl.add partitions pid row in
+ (try
+ List.iter2 add pidl t
+ with Invalid_argument _ -> assert false);
+ let pidset = int_set_of_int_list pidl in
+ IntSet.fold
+ (fun pid acc ->
+ match Hashtbl.find_all partitions pid with
+ | [] -> acc
+ | patterns -> (pid, List.rev patterns) :: acc)
+ pidset []
+
+ let are_empty t = fst (List.hd t) = []
+ (* if first row has an empty list of patterns, then others will as well *)
+
+ (* return 2 lists of rows, first one containing homogeneous rows according
+ * to "compatible" below *)
+ let horizontal_split t =
+ let ap =
+ match t with
+ | [] -> assert false
+ | ([], _) :: _ ->
+ assert false (* are_empty should have been invoked in advance *)
+ | (hd :: _ , _) :: _ -> hd
+ in
+ let rec aux prev_t = function
+ | [] -> List.rev prev_t, []
+ | ([], _) :: _ -> assert false
+ | (((hd :: _), _) as row) :: tl when P.compatible ap hd ->
+ aux (row :: prev_t) tl
+ | t -> List.rev prev_t, t
+ in
+ aux [] t
- with Invalid_argument _ -> assert false
+ (* return 2 lists, first one representing first column, second one
+ * representing rows stripped of the first element *)
+ let vertical_split t =
+ let l =
+ List.map
+ (function
+ | (hd :: tl, pid) -> hd, (tl, pid)
+ | _ -> assert false)
+ t
+ in
+ List.split l
+ end
+
+module Patterns21 = Patterns (CicNotationTag)
- let prepend_columns t columns =
- List.fold_right
- (fun column rows -> prepend_column rows column)
- columns t
+module Patterns32 =
+ struct
+ type row_t = CicNotationPt.cic_appl_pattern list * pattern_id
+ type t = row_t list
+
+ let empty = []
+
+ let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t
+ let pattern_ids t = List.map snd t
let partition t pidl =
let partitions = Hashtbl.create 11 in
let idref id t = Ast.AttributedTerm (`IdRef id, t)
+let pp_ast0 t k =
+ prerr_endline "pp_ast0";
+ let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+ and special_k = function
+ | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+ | _ -> assert false
+ in
+ aux t
+
let ast_of_acic0 term_info acic k =
(* prerr_endline "ast_of_acic0"; *)
let k = k term_info in
(* persistent state *)
-let level2_patterns = Hashtbl.create 211
+let level1_patterns21 = Hashtbl.create 211
+let level2_patterns32 = Hashtbl.create 211
+let (compiled21: (CicNotationPt.term -> CicNotationPt.term) option ref) =
+ ref None
let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
ref None
-let pattern_matrix = ref Patterns.empty
+let pattern21_matrix = ref Patterns21.empty
+let pattern32_matrix = ref Patterns32.empty
+let get_compiled21 () =
+ match !compiled21 with
+ | None -> assert false
+ | Some f -> f
let get_compiled32 () =
match !compiled32 with
| None -> assert false
| Some f -> f
+let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
(* "envl" is a list of triples:
end))
(* compiler from level 3 to level 2 *)
-let compiler32 (t: Patterns.t) success_k fail_k =
+let compiler32 (t: Patterns32.t) success_k fail_k =
let rec aux t k = (* k is a continuation *)
if t = [] then
k
- else if Patterns.are_empty t then begin
+ else if Patterns32.are_empty t then begin
(match t with
| _::_::_ ->
- (* optimization possible here: throw away all except one of the rules
- * which lead to ambiguity *)
- warning "Ambiguous patterns"
+ (* XXX optimization possible here: throw away all except one of the
+ * rules which lead to ambiguity *)
+ warning "ambiguous interpretation"
| _ -> ());
return_closure success_k
end else
- match Patterns.horizontal_split t with
+ match Patterns32.horizontal_split t with
| t', [] ->
(match t' with
| []
| ([], _) :: _ -> assert false
| (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _
| (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ ->
- let first_column, t'' = Patterns.vertical_split t' in
+ let first_column, t'' = Patterns32.vertical_split t' in
let names =
List.map
(function
t'
in
(* arity partitioning *)
- let clusters = Patterns.partition t' pidl in
+ let clusters = Patterns32.partition t' pidl in
let ks = (* k continuation list *)
List.map
(fun (len, cluster) ->
in
!uidmap, uidl
in
- let clusters = Patterns.partition t' pidl in
+ let clusters = Patterns32.partition t' pidl in
let ks =
List.map
(fun (uid, cluster) ->
matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t)
with No_match -> fail_k term_info annterm)
+let return_closure21 success_k =
+ (fun terms envl ->
+ prerr_endline "return_closure21";
+ match terms with
+ | [] ->
+ (try
+ success_k (List.hd envl)
+ with Failure _ -> assert false)
+ | _ -> assert false)
+
+let variable_closure21 vars k =
+ (fun terms envl ->
+ prerr_endline "variable_closure21";
+ match terms with
+ | hd :: tl ->
+ let envl' =
+ List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars envl
+ in
+ k tl envl'
+ | _ -> assert false)
+
+let constructor_closure21 ks k =
+ (fun terms envl ->
+ prerr_endline "constructor_closure21";
+ (match terms with
+ | p :: tl ->
+ prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term p));
+ (try
+ let tag, subterms = CicNotationTag.get_tag p in
+ let k' = List.assoc tag ks in
+ k' (subterms @ tl) envl
+ with Not_found -> k terms envl)
+ | [] -> assert false))
+
+let compiler21 (t: Patterns21.t) success_k fail_k =
+ let rec aux t k =
+ if t = [] then
+ k
+ else if Patterns21.are_empty t then begin
+ (match t with
+ | _::_::_ ->
+ (* XXX optimization possible here: throw away all except one of the
+ * rules which lead to ambiguity *)
+ warning "ambiguous notation"
+ | _ -> ());
+ return_closure21 success_k
+ end else
+ match Patterns21.horizontal_split t with
+ | t', [] ->
+ (match t' with
+ | []
+ | ([], _) :: _ -> assert false
+ | (Ast.Variable _ :: _, _) :: _ ->
+ let first_column, t'' = Patterns21.vertical_split t' in
+ let vars =
+ List.map
+ (function
+ | Ast.Variable v -> v
+ | _ -> assert false)
+ first_column
+ in
+ variable_closure21 vars (aux t'' k)
+ | _ ->
+ let pidl =
+ List.map
+ (function
+ | p :: _, _ -> fst (CicNotationTag.get_tag p)
+ | [], _ -> assert false)
+ t'
+ in
+ let clusters = Patterns21.partition t' pidl in
+ let ks =
+ List.map
+ (fun (pid, cluster) ->
+ let cluster' =
+ List.map (* add args as patterns heads *)
+ (function
+ | p :: tl, pid ->
+ let _, subpatterns = CicNotationTag.get_tag p in
+ subpatterns @ tl, pid
+ | _ -> assert false)
+ cluster
+ in
+ pid, aux cluster' k)
+ clusters
+ in
+ constructor_closure21 ks k)
+ | t', tl -> aux t' (aux tl k)
+ in
+ let matcher = aux t (fun _ _ -> raise No_match) in
+ (fun ast ->
+ try
+ matcher [ast] (List.map (fun (_, pid) -> [], pid) t)
+ with No_match -> fail_k ast)
+
let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm
-let instantiate term_info name_env term_env pid =
+let pp_ast1 term = (get_compiled21 ()) term
+
+let instantiate21 env pid =
+ prerr_endline "instantiate21";
+ let precedence, associativity, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ let rec subst = function
+ | Ast.AttributedTerm (_, t) -> subst t
+ | Ast.Variable var ->
+ (try List.assoc var env with Not_found -> assert false)
+ | (Ast.Literal _
+ | Ast.Magic _) as t -> t
+ | Ast.Layout l -> Ast.Layout (subst_layout l)
+ | t -> CicNotationUtil.visit_ast subst t
+ and subst_layout l = CicNotationUtil.visit_layout subst l in
+ subst l1
+
+let instantiate32 term_info name_env term_env pid =
let symbol, args =
try
- Hashtbl.find level2_patterns pid
+ Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
in
let rec instantiate_arg = function
let args' = List.map instantiate_arg args in
Ast.Appl (Ast.Symbol (symbol, 0) :: args')
-let load_patterns t =
+let load_patterns32 t =
let ast_env_of_name_env term_info name_env =
List.map
(fun (name, (name', ty_opt)) ->
in
let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in
let success_k term_info (name_env, term_env, pid) =
- instantiate
+ instantiate32
term_info
(ast_env_of_name_env term_info name_env)
(ast_env_of_term_env term_info term_env)
let compiled32 = compiler32 t success_k fail_k in
set_compiled32 compiled32
+let load_patterns21 t =
+ let ast_env_of_env env =
+ List.map (fun (var, term) -> (var, pp_ast1 term)) env
+ in
+ let fail_k term = pp_ast0 term pp_ast1 in
+ let success_k (env, pid) = instantiate21 (ast_env_of_env env) pid in
+ let compiled21 = compiler21 t success_k fail_k in
+ set_compiled21 compiled21
+
let ast_of_acic id_to_sort annterm =
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast = ast_of_acic1 term_info annterm in
ast, term_info.uri
+let pp_ast term = pp_ast1 term
+
let fresh_id =
let counter = ref ~-1 in
fun () ->
let add_interpretation (symbol, args) appl_pattern =
let id = fresh_id () in
- Hashtbl.add level2_patterns id (symbol, args);
- pattern_matrix := ([appl_pattern], id) :: !pattern_matrix;
- load_patterns !pattern_matrix;
+ Hashtbl.add level2_patterns32 id (symbol, args);
+ pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix;
+ load_patterns32 !pattern32_matrix;
+ id
+
+let add_pretty_printer ?precedence ?associativity l2 l1 =
+ let id = fresh_id () in
+ let l2' = CicNotationUtil.strip_attributes l2 in
+ Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
+ pattern21_matrix := ([l2'], id) :: !pattern21_matrix;
+ load_patterns21 !pattern21_matrix;
id
exception Interpretation_not_found
+exception Pretty_printer_not_found
let remove_interpretation id =
(try
- Hashtbl.remove level2_patterns id;
+ Hashtbl.remove level2_patterns32 id;
with Not_found -> raise Interpretation_not_found);
- pattern_matrix := List.filter (fun (_, id') -> id <> id') !pattern_matrix;
- load_patterns !pattern_matrix
+ pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;
+ load_patterns32 !pattern32_matrix
-let _ = load_patterns []
+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 _ =
+ load_patterns21 [];
+ load_patterns32 []
projects / helm.git / blobdiff