parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / universe.ml

diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml
index c8d370f04ff8807f08cbf2afd6a12459bd42af63..d20dbda352acf9ed2a59adeff810352c6993ada8 100644 (file)
--- a/helm/software/components/tactics/universe.ml
+++ b/helm/software/components/tactics/universe.ml
@@ -28,20 +28,39 @@ module Codomain = struct
   let compare = Pervasives.compare 
 end
 module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
+module TI = Discrimination_tree.Make(Cic_indexable.CicIndexable)(S)
 type universe = TI.t
 
-let empty = TI.empty
+let empty = TI.empty ;;
+
+let iter u f = 
+  TI.iter u 
+   (fun p s -> f p (S.elements s))
 ;;
 
 let get_candidates univ ty = 
   S.elements (TI.retrieve_unifiables univ ty)
 ;;
 
+let in_universe univ ty =
+  let candidates = get_candidates univ ty in
+    List.fold_left 
+      (fun res cand ->
+        match res with
+          | Some found -> Some found
+          | None -> 
+              let candty,_ = 
+                CicTypeChecker.type_of_aux' [] [] cand CicUniv.oblivion_ugraph in
+              let same ,_ = 
+                CicReduction.are_convertible [] candty ty CicUniv.oblivion_ugraph in
+              if same then Some cand else None
+      ) None candidates
+;;
+
 let rec unfold context = function
   | Cic.Prod(name,s,t) -> 
       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
-       Cic.Prod(name,s,t')     
+        Cic.Prod(name,s,t')        
   | t -> ProofEngineReduction.unfold context t
 
 let rec collapse_head_metas t = 
@@ -73,26 +92,28 @@ let rec collapse_head_metas t =
 
 let rec dummies_of_coercions = 
   function
-    | Cic.Appl (c::l) when CoercDb.is_a_coercion' c ->
-       Cic.Meta (-1,[])
+    | Cic.Appl (c::l) when CoercDb.is_a_coercion c <> None ->
+        Cic.Meta (-1,[])
     | Cic.Appl l -> 
-       let l' = List.map dummies_of_coercions l in Cic.Appl l'
+        let l' = List.map dummies_of_coercions l in Cic.Appl l'
     | Cic.Lambda(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.Lambda (n,s',t')
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Lambda (n,s',t')
     | Cic.Prod(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.Prod (n,s',t')    
-    | Cic.LetIn(n,s,t) ->
-       let s' = dummies_of_coercions s in
-       let t' = dummies_of_coercions t in
-         Cic.LetIn (n,s',t')   
-    | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[])
+        let s' = dummies_of_coercions s in
+        let t' = dummies_of_coercions t in
+          Cic.Prod (n,s',t')        
+    | Cic.LetIn(n,s,ty,t) ->
+        let s' = dummies_of_coercions s in
+        let ty' = dummies_of_coercions ty in
+        let t' = dummies_of_coercions t in
+          Cic.LetIn (n,s',ty',t')        
+    | Cic.MutCase _ -> Cic.Meta (-1,[])
     | t -> t
 ;;
 
+
 let rec head remove_coercions t = 
   let clean_up t =
     if remove_coercions then dummies_of_coercions t
@@ -118,6 +139,8 @@ let keys context ty =
     [head true ty; head true (unfold context ty)]
   with ProofEngineTypes.Fail _ -> [head true ty]
 
+let key term = head false term;;
+
 let index_term_and_unfolded_term univ context t ty =
   let key = head true ty in
   let univ = index univ key t in
@@ -158,7 +181,7 @@ let remove univ context term ty =
 
 let remove_uri univ uri =
   let term = CicUtil.term_of_uri uri in
-  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+  let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
     remove univ [] term ty