]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationRew.ml
version 0.7.1
[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml
index 7dd97398920e75cceba8d365934da37740af3365..2f95a56350f5af1b5fa492c36d2310fa18debb18 100644 (file)
@@ -34,156 +34,8 @@ type term_info =
     uri: (Cic.id, string) Hashtbl.t;
   }
 
-exception No_match
-
-module OrderedInt =
-  struct
-  type t = int
-  let compare (x1:t) (x2:t) = Pervasives.compare x2 x1  (* reverse order *)
-  end
-
-module IntSet = Set.Make (OrderedInt)
-
-let int_set_of_int_list l =
-  List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l
-
 let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
 
-module type PATTERN =
-  sig
-  type pattern_t
-  val compatible : pattern_t -> pattern_t -> bool
-  end
-
-module Patterns (P: PATTERN) =
-  struct
-  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 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, first_row, t' =
-      match t with
-      | [] -> assert false
-      | ([], _) :: _ ->
-          assert false  (* are_empty should have been invoked in advance *)
-      | ((hd :: _ , _) as row) :: tl -> hd, row, tl
-    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 [first_row] t'
-
-    (* 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)
-
-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 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 compatible ap1 ap2 =
-      match ap1, ap2 with
-      | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _
-      | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _
-      | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true
-      | _ -> false
-    in
-    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 compatible ap hd ->
-          aux (row :: prev_t) tl
-      | t -> List.rev prev_t, t
-    in
-    aux [] t
-
-    (* 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
-
-  (* acic -> ast auxiliary function s *)
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -210,6 +62,7 @@ let constructor_of_inductive_type uri i j =
   with Not_found -> assert false)
 
 module Ast = CicNotationPt
+module Parser = CicNotationParser
 
 let string_of_name = function
   | Cic.Name s -> s
@@ -219,11 +72,41 @@ let ident_of_name n = Ast.Ident (string_of_name n, None)
 
 let idref id t = Ast.AttributedTerm (`IdRef id, t)
 
+let resolve_binder = function
+  | `Lambda -> "\\lambda"
+  | `Pi -> "\\Pi"
+  | `Forall -> "\\forall"
+  | `Exists -> "\\exists"
+
 let pp_ast0 t k =
-  prerr_endline "pp_ast0";
-  let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+  let rec aux = function
+    | Ast.Appl ts ->
+        Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
+          Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts)))
+    | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body)
+    | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) ->
+        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            aux_ty ty;
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol "\\to"); k body]))])))
+    | Ast.Binder (binder_kind, (id, ty), body) ->
+        Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
+          Ast.Layout (Ast.Box ((Ast.HV, false, true), [
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol (resolve_binder binder_kind));
+              k id;
+              Ast.Literal (`Symbol ":");
+              aux_ty ty ]));
+            Ast.Layout (Ast.Box ((Ast.H, false, false), [
+              Ast.Literal (`Symbol ".");
+              k body ]))])))
+    | t -> CicNotationUtil.visit_ast ~special_k k t
+  and aux_ty = function
+    | None -> Ast.Literal (`Symbol "?")
+    | Some ty -> k ty
   and special_k = function
-    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+    | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t)
     | _ -> assert false
   in
   aux t
@@ -347,13 +230,15 @@ let ast_of_acic0 term_info acic k =
 let level1_patterns21 = Hashtbl.create 211
 let level2_patterns32 = Hashtbl.create 211
 
-let (compiled21: (CicNotationPt.term -> CicNotationPt.term) option ref) =
+let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option)
+option ref) =
   ref None
-let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
+let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option)
+option ref) =
   ref None
 
-let pattern21_matrix = ref Patterns21.empty
-let pattern32_matrix = ref Patterns32.empty
+let pattern21_matrix = ref []
+let pattern32_matrix = ref []
 
 let get_compiled21 () =
   match !compiled21 with
@@ -367,295 +252,11 @@ let get_compiled32 () =
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-  (* "envl" is a list of triples:
-   *   <name environment, term environment, pattern id>, where
-   *   name environment: (string * string) list
-   *   term environment: (string * Cic.annterm) list *)
-let return_closure success_k =
-  (fun term_info terms envl ->
-(*     prerr_endline "return_closure"; *)
-    match terms with
-    | [] ->
-        (try
-          success_k term_info (List.hd envl)
-        with Failure _ -> assert false)
-    | _ -> assert false)
-
-let variable_closure names k =
-  (fun term_info terms envl ->
-(*     prerr_endline "variable_closure"; *)
-    match terms with
-    | hd :: tl ->
-        let envl' =
-          List.map2
-            (fun arg (name_env, term_env, pid) ->
-              let rec aux name_env term_env pid arg term =
-                match arg, term with
-                  Ast.IdentArg name, _ ->
-                    (name_env, (name, term) :: term_env, pid)
-                | Ast.EtaArg (Some name, arg'),
-                  Cic.ALambda (id, name', ty, body) ->
-                    aux
-                      ((name, (string_of_name name', Some (ty, id))) :: name_env)
-                      term_env pid arg' body
-                | Ast.EtaArg (Some name, arg'), _ ->
-                    let name' = CicNotationUtil.fresh_name () in
-                    aux ((name, (name', None)) :: name_env)
-                      term_env pid arg' term
-                | Ast.EtaArg (None, arg'), Cic.ALambda (id, name, ty, body) ->
-                    assert false
-                | Ast.EtaArg (None, arg'), _ ->
-                    assert false
-              in
-                aux name_env term_env pid arg hd)
-            names envl
-        in
-        k term_info tl envl'
-    | _ -> assert false)
-
-let appl_closure ks k =
-  (fun term_info terms envl ->
-(*     prerr_endline "appl_closure"; *)
-    (match terms with
-    | Cic.AAppl (_, args) :: tl ->
-        (try
-          let k' = List.assoc (List.length args) ks in
-          k' term_info (args @ tl) envl
-        with Not_found -> k term_info terms envl)
-    | [] -> assert false
-    | _ -> k term_info terms envl))
-
-let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
-
-let uri_closure ks k =
-  (fun term_info terms envl ->
-(*     prerr_endline "uri_closure"; *)
-    (match terms with
-    | [] -> assert false
-    | hd :: tl ->
-(*         prerr_endline (sprintf "uri_of_term = %s" (uri_of_term hd)); *)
-        begin
-          try
-            let k' = List.assoc (uri_of_term hd) ks in
-            k' term_info tl envl
-          with
-          | Invalid_argument _  (* raised by uri_of_term *)
-          | Not_found -> k term_info terms envl
-        end))
-
-  (* compiler from level 3 to level 2 *)
-let compiler32 (t: Patterns32.t) success_k fail_k =
-  let rec aux t k = (* k is a continuation *)
-    if t = [] then
-      k
-    else if Patterns32.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 interpretation"
-      | _ -> ());
-      return_closure success_k
-    end else
-      match Patterns32.horizontal_split t with
-      | t', [] ->
-          (match t' with
-          | []
-          | ([], _) :: _ -> assert false
-          | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _
-          | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ ->
-              let first_column, t'' = Patterns32.vertical_split t' in
-              let names =
-                List.map
-                  (function
-                    | Ast.ArgPattern arg -> arg
-                    | _ -> assert false)
-                  first_column
-              in
-              variable_closure names (aux t'' k)
-          | (Ast.ApplPattern _ :: _, _) :: _ ->
-              let pidl =
-                List.map
-                  (function
-                    | (Ast.ApplPattern args) :: _, _ -> List.length args
-                    | _ -> assert false)
-                  t'
-              in
-                (* arity partitioning *)
-              let clusters = Patterns32.partition t' pidl in
-              let ks =  (* k continuation list *)
-                List.map
-                  (fun (len, cluster) ->
-                    let cluster' =
-                      List.map  (* add args as patterns heads *)
-                        (function
-                          | (Ast.ApplPattern args) :: tl, pid ->
-                              (* let's throw away "teste di cluster" *)
-                              args @ tl, pid
-                          | _ -> assert false)
-                        cluster
-                    in
-                    len, aux cluster' k)
-                  clusters
-              in
-              appl_closure ks k
-          | (Ast.UriPattern _ :: _, _) :: _ ->
-              let uidmap, pidl =
-                let urimap = ref [] in
-                let uidmap = ref [] in
-                let get_uri_id uri =
-                  try
-                    List.assoc uri !urimap
-                  with
-                    Not_found ->
-                      let uid = List.length !urimap in
-                      urimap := (uri, uid) :: !urimap ;
-                      uidmap := (uid, uri) :: !uidmap ;
-                      uid
-                in
-                let uidl =
-                  List.map
-                    (function
-                      | (Ast.UriPattern uri) :: _, _ -> get_uri_id uri
-                      | _ -> assert false)
-                    t'
-                in
-                  !uidmap, uidl
-              in
-              let clusters = Patterns32.partition t' pidl in
-              let ks =
-                List.map
-                  (fun (uid, cluster) ->
-                    let cluster' =
-                      List.map
-                        (function
-                        | (Ast.UriPattern uri) :: tl, pid -> tl, pid
-                        | _ -> assert false)
-                      cluster
-                    in
-                    List.assoc uid uidmap, aux cluster' k)
-                  clusters
-              in
-              uri_closure ks k)
-      | t', tl -> aux t' (aux tl k)
-  in
-  let matcher = aux t (fun _ _ -> raise No_match) in
-  (fun term_info annterm ->
-    try
-      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 (name, ty) (env, pid) ->
-              (name, (ty, CicNotationEnv.value_of_term 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 -> CicNotationEnv.declaration_of_var 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 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
+let instantiate21 env precedence associativity l1 =
+  let rec subst_singleton env t =
+    CicNotationUtil.boxify (subst env t)
+  and subst env = function
+    | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
         let ty, value =
@@ -667,65 +268,62 @@ let instantiate21 env pid =
         (* following assertion should be a conditional that makes this
          * instantiation fail *)
         assert (CicNotationEnv.well_typed expected_ty value);
-        CicNotationEnv.term_of_value value
-    | Ast.Magic _ -> assert false (* TO BE IMPLEMENTED *)
-    | Ast.Literal _ 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_patterns32 pid
-    with Not_found -> assert false
-  in
-  let rec instantiate_arg = function
-    | Ast.IdentArg name ->
-        (try List.assoc name term_env with Not_found -> assert false)
-    | Ast.EtaArg (None, _) -> assert false  (* TODO *)
-    | Ast.EtaArg (Some name, arg) ->
-        let (name', ty_opt) =
-          try List.assoc name name_env with Not_found -> assert false
+        [ CicNotationEnv.term_of_value value ]
+    | Ast.Magic m -> subst_magic env m
+    | Ast.Literal _ as t -> [ t ]
+    | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
+    | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
+  and subst_magic env = function
+    | Ast.List0 (p, sep_opt)
+    | Ast.List1 (p, sep_opt) ->
+        let rec_decls = CicNotationEnv.declarations_of_term p in
+        let rec_values =
+          List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls
         in
-        let body = instantiate_arg arg in
-        let name' = Ast.Ident (name', None) in
-        match ty_opt with
-        | None -> Ast.Binder (`Lambda, (name', None), body)
-        | Some (ty, id) ->
-            idref id (Ast.Binder (`Lambda, (name', Some ty), body))
-  in
-  let args' = List.map instantiate_arg args in
-  Ast.Appl (Ast.Symbol (symbol, 0) :: args')
-
-let load_patterns32 t =
-  let ast_env_of_name_env term_info name_env =
-    List.map
-      (fun (name, (name', ty_opt)) ->
-        let ast_ty_opt =
-          match ty_opt with
-          | None -> None
-          | Some (annterm, id) -> Some (ast_of_acic1 term_info annterm, id)
+        let values = CicNotationUtil.ncombine rec_values in
+        let sep =
+          match sep_opt with
+          | None -> []
+          | Some l -> [ CicNotationPt.Literal l ]
         in
-        (name, (name', ast_ty_opt)))
-      name_env
-  in
-  let ast_env_of_term_env term_info =
-    List.map (fun (name, term) -> (name, ast_of_acic1 term_info term))
-  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) =
-    instantiate32
-      term_info
-      (ast_env_of_name_env term_info name_env)
-      (ast_env_of_term_env term_info term_env)
-      pid
+        let rec instantiate_list acc = function
+          | [] -> List.rev acc
+         | value_set :: [] ->
+             let env = CicNotationEnv.combine rec_decls value_set in
+               instantiate_list
+                  ((CicNotationUtil.boxify (subst env p)) :: acc) []
+          | value_set :: tl ->
+              let env = CicNotationEnv.combine rec_decls value_set in
+              instantiate_list
+                ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
+        in
+        instantiate_list [] values
+    | Ast.Opt p ->
+        let opt_decls = CicNotationEnv.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
+                | None -> raise Exit
+                | Some v -> (name, (ty, v)) :: build_env tl)
+          in
+          try build_env opt_decls with Exit -> []
+        in
+         begin
+           match env with
+             | [] -> []
+             | _ -> subst env p
+         end
+    | _ -> assert false (* impossible *)
+  and subst_layout env = function
+    | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
-  let compiled32 = compiler32 t success_k fail_k in
-  set_compiled32 compiled32
+    subst_singleton env l1
 
-let load_patterns21 t =
+let rec pp_ast1 term = 
   let rec pp_value = function
     | CicNotationEnv.NumValue _ as v -> v
     | CicNotationEnv.StringValue _ as v -> v
@@ -739,10 +337,56 @@ let load_patterns21 t =
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) 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
+  match (get_compiled21 ()) term with
+  | None -> pp_ast0 term pp_ast1
+  | Some (env, pid) ->
+      let precedence, associativity, l1 =
+        try
+          Hashtbl.find level1_patterns21 pid
+        with Not_found -> assert false
+      in
+      instantiate21 (ast_env_of_env env) precedence associativity l1
+
+let instantiate32 term_info env symbol args =
+  let rec instantiate_arg = function
+    | Ast.IdentArg (n, name) ->
+        let t = (try List.assoc name env with Not_found -> assert false) in
+        let rec count_lambda = function
+          | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
+          | _ -> 0
+        in
+        let rec add_lambda t n =
+          if n > 0 then
+            let name = CicNotationUtil.fresh_name () in
+            Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
+              Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
+          else
+            t
+        in
+        add_lambda t (n - count_lambda t)
+  in
+  let args' = List.map instantiate_arg args in
+  Ast.Appl (Ast.Symbol (symbol, 0) :: args')
+
+let rec ast_of_acic1 term_info annterm = 
+  match (get_compiled32 ()) annterm with
+  | None -> ast_of_acic0 term_info annterm ast_of_acic1
+  | Some (env, pid) -> 
+      let env' =
+        List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
+      in
+      let symbol, args =
+        try
+          Hashtbl.find level2_patterns32 pid
+        with Not_found -> assert false
+      in
+      instantiate32 term_info env' symbol args
+
+let load_patterns32 t =
+  set_compiled32 (CicNotationMatcher.Matcher32.compiler t)
+
+let load_patterns21 t =
+  set_compiled21 (CicNotationMatcher.Matcher21.compiler t)
 
 let ast_of_acic id_to_sort annterm =
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
@@ -760,7 +404,7 @@ let fresh_id =
 let add_interpretation (symbol, args) appl_pattern =
   let id = fresh_id () in
   Hashtbl.add level2_patterns32 id (symbol, args);
-  pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix;
+  pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix;
   load_patterns32 !pattern32_matrix;
   id
 
@@ -768,7 +412,7 @@ 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;
+  pattern21_matrix := (l2', id) :: !pattern21_matrix;
   load_patterns21 !pattern21_matrix;
   id