prima implementazione di demodulate, superposition_left e superposition_right

[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 2e2d8c9d45f3699180658824d40b00939c5bb66a..151ec8a08516cf8074fe6aad4483a662be46d0ff 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -221,15 +221,12 @@ let get_compiled32 () =
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-let instantiate21 env pid =
+let instantiate21 env precedence associativity l1 =
   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 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 =
@@ -241,13 +238,60 @@ 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
+        [ 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 values = CicNotationUtil.ncombine rec_values in
+        let sep =
+          match sep_opt with
+          | None -> []
+          | Some l -> [ CicNotationPt.Literal l ]
+        in
+        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
+    subst_singleton env l1
 
 let rec pp_ast1 term = 
   let rec pp_value = function
@@ -265,7 +309,13 @@ let rec pp_ast1 term =
   in
   match (get_compiled21 ()) term with
   | None -> pp_ast0 term pp_ast1
-  | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid
+  | 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