1 files changed, 118 insertions, 0 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
new file mode 100644
index 000000000..4f86af1e8
--- /dev/null
+++ b/contrib/subtac/eterm.ml
@@ -0,0 +1,118 @@
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+open Term
+open Names
+open Sutils
+open Evd
+open List
+open Pp
+(** Substitute evar references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_evars evs n t = 
+  let evar_index id = 
+    let idx = list_assoc_index id evs in
+      idx + 1
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Evar (k, args) ->
+	(try 
+	   msgnl (str "Evar " ++ int k ++ str " found");
+	   let ex = 
+(* 	     mkVar (id_of_string ("Evar" ^ string_of_int k));*)
+  	     mkRel (evar_index k + depth)  
+	   in
+	   let args = Array.map (map_constr_with_binders succ substrec depth) args in
+	     mkApp (ex, args)
+	 with Not_found -> 
+	   msgnl (str "Evar " ++ int k ++ str " not found!!!");
+	   c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+      
+(** Substitute variable references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_vars acc n t = 
+  let var_index id = 
+    let idx = list_index id acc in
+      idx + 1
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+  to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+  Changes evars and hypothesis references to De Bruijn indices.
+*)
+let etype_of_evar evs ev =
+  let rec aux acc n = function
+      (id, copt, t) :: tl ->
+	let t' = subst_evars evs n t in
+	let t'' = subst_vars acc 0 t' in
+ 	  mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
+    | [] ->
+	let t' = subst_evars evs n ev.evar_concl in
+	  subst_vars acc 0 t'	
+  in aux [] 0 (rev ev.evar_hyps)
+
+
+open Tacticals
+    
+let eterm evm t = 
+  (* 'Serialize' the evars, we assume that the types of the existentials
+     refer to previous existentials in the list only *)
+  let evl = to_list evm in
+  let evts = 
+    (* Remove existential variables in types and build the corresponding products *)
+    fold_left 
+      (fun l (id, y) -> 
+	 let y' = (id, etype_of_evar l y) in
+	   y' :: l) 
+      [] evl 
+  in 
+  let t' = (* Substitute evar refs in the term to De Bruijn indices *)
+    subst_evars evts 0 t 
+  in
+  let t'' = 
+    (* Make the lambdas 'generalizing' the existential variables *)
+    fold_left
+      (fun acc (id, c) ->
+	 mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
+		   c, acc))
+      t' evts
+      
+
+  in
+  let declare_evar (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
+					  Decl_kinds.IsAssumption Decl_kinds.Definitional))
+  in
+  let declare_assert acc (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      tclTHEN acc (Tactics.assert_tac false (Name id) c)
+  in
+    msgnl (str "Term constructed in Eterm" ++
+	   Termops.print_constr_env (Global.env ()) t'');
+   Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts)
+    (* t'' *)
+    (* Hack: push evars as assumptions in the global env *)
+(*     iter declare_evar evts; *)
+(*     Tactics.apply t' *)
+    (*tclTHEN (fold_left declare_assert tclIDTAC evts) (Tactics.apply t')*)
+       
+open Tacmach
+
+let etermtac (evm, t) = 
+  let t' = eterm evm t in
+    t'
+(*     Tactics.apply (Reduction.nf_betaiota t') 
+    Tactics.exact (Reduction.nf_betaiota t')*)