snapshot (added typed environment in 2 -> 1 conversion)

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index e037ca2a97e4b621d2c2b7ac9c663ffe2581b764..7dd97398920e75cceba8d365934da37740af3365 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -85,12 +85,12 @@ module Patterns (P: PATTERN) =
     (* return 2 lists of rows, first one containing homogeneous rows according
      * to "compatible" below *)
   let horizontal_split t =
-    let ap =
+    let ap, first_row, t' =
       match t with
       | [] -> assert false
       | ([], _) :: _ ->
           assert false  (* are_empty should have been invoked in advance *)
-      | (hd :: _ , _) :: _ -> hd
+      | ((hd :: _ , _) as row) :: tl -> hd, row, tl
     in
     let rec aux prev_t = function
       | [] -> List.rev prev_t, []
@@ -99,7 +99,7 @@ module Patterns (P: PATTERN) =
           aux (row :: prev_t) tl
       | t -> List.rev prev_t, t
     in
-    aux [] t
+    aux [first_row] t'
 
     (* return 2 lists, first one representing first column, second one
      * representing rows stripped of the first element *)
@@ -561,7 +561,10 @@ let variable_closure21 vars k =
     match terms with
     | hd :: tl ->
         let envl' =
-          List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars 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)
@@ -602,7 +605,7 @@ let compiler21 (t: Patterns21.t) success_k fail_k =
               let vars =
                 List.map
                   (function
-                    | Ast.Variable v -> v
+                    | Ast.Variable v -> CicNotationEnv.declaration_of_var v
                     | _ -> assert false)
                   first_column
               in
@@ -654,9 +657,19 @@ let instantiate21 env pid =
   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
+        let name, expected_ty = CicNotationEnv.declaration_of_var var in
+        let ty, value =
+          try
+            List.assoc name env
+          with Not_found -> assert false
+        in
+        assert (CicNotationEnv.well_typed ty value); (* INVARIANT *)
+        (* 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
@@ -713,8 +726,18 @@ let load_patterns32 t =
   set_compiled32 compiled32
 
 let load_patterns21 t =
+  let rec pp_value = function
+    | CicNotationEnv.NumValue _ as v -> v
+    | CicNotationEnv.StringValue _ as v -> v
+    | 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)
+  in
   let ast_env_of_env env =
-    List.map (fun (var, term) -> (var, pp_ast1 term)) 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