First commit of our future proof-assistant/proof-improver (???)

[helm.git] / helm / gTopLevel / logicalOperations.ml

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
new file mode 100644 (file)
index 0000000..6644250
--- /dev/null
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -0,0 +1,73 @@
+let get_parent id ids_to_terms ids_to_father_ids =
+ match Hashtbl.find ids_to_father_ids id with
+    None -> None
+  | Some id -> Some (id, Hashtbl.find ids_to_terms id)
+;;
+
+let get_context ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+ let module C = Cic in
+  let rec aux id =
+   match get_parent id ids_to_terms ids_to_father_ids with
+      None -> []
+    | Some (parentid,parent) ->
+       let term = Hashtbl.find ids_to_terms id in
+       let binding =
+        match parent with
+           C.Rel _
+         | C.Var _
+         | C.Meta _
+         | C.Sort _
+         | C.Implicit
+         | C.Cast _ -> []
+         | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
+         | C.Prod _ -> []
+         | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
+         | C.Lambda _ -> []
+         | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
+         | C.LetIn _ -> []
+         | C.Appl _
+         | C.Const _ -> []
+         | C.Abst _ -> assert false
+         | C.MutInd _
+         | C.MutConstruct _
+         | C.MutCase _ -> []
+(*CSC: sbagliato: manca il when *)
+         | C.Fix (_,ifl) ->
+            let counter = ref 0 in
+             List.rev_map
+              (function (name,_,ty,bo) ->
+                let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
+                 incr counter ;
+                 res
+              ) ifl
+         | C.CoFix (_,ifl) ->
+            let counter = ref 0 in
+             List.rev_map
+              (function (name,ty,bo) ->
+                let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
+                 incr counter ;
+                 res
+              ) ifl
+       in
+        binding@(aux parentid)
+  in
+   aux
+;;
+
+exception NotImplemented;;
+
+let to_sequent id ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+  let term = Hashtbl.find ids_to_terms id in
+  let context = get_context ids_to_terms ids_to_father_ids id in
+   let type_checker_env_of_context =
+    List.map
+     (function
+         P.Declaration,_,t -> t
+       | P.Definition,_,_ -> raise NotImplemented
+     ) context
+   in
+    let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in
+     ((context,ty) : ProofEngine.sequent)
+;;