X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=e037ca2a97e4b621d2c2b7ac9c663ffe2581b764;hb=dbcc29c0e46454c7e31b485135900ceab38627e1;hp=b979e84c99f255aa313a3382106455d79d7702ad;hpb=7d425434a70ed1eae2ef83ebff5adbbbeeaec099;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index b979e84c9..e037ca2a9 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -27,6 +27,7 @@ open Printf
 
 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;
@@ -48,9 +49,15 @@ let int_set_of_int_list l =
 
 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 = []
@@ -58,16 +65,66 @@ module Patterns =
   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
@@ -162,6 +219,15 @@ let ident_of_name n = Ast.Ident (string_of_name n, None)
 
 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
@@ -278,18 +344,27 @@ let ast_of_acic0 term_info acic k =
 
   (* 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:
@@ -369,27 +444,27 @@ let uri_closure ks k =
         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
@@ -407,7 +482,7 @@ let compiler32 (t: Patterns.t) success_k fail_k =
                   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) ->
@@ -447,7 +522,7 @@ let compiler32 (t: Patterns.t) success_k fail_k =
                 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) ->
@@ -470,12 +545,127 @@ let compiler32 (t: Patterns.t) success_k fail_k =
       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
@@ -496,7 +686,7 @@ let instantiate term_info name_env term_env pid =
   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)) ->
@@ -513,7 +703,7 @@ let load_patterns t =
   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)
@@ -522,11 +712,22 @@ let load_patterns t =
   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 () ->
@@ -535,19 +736,37 @@ let fresh_id =
 
 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 []