* The interface of CicTypeChecker now allows the usage of definitions in

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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 8f5d0c96e9ef749811d7370a33fc3be52984811c..29a23a191b4bbfbf1eb9235c761e0395385614d7 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -1,13 +1,13 @@
 type binder_type =
-   Declaration
- | Definition
+   Declaration of Cic.name * Cic.term
+ | Definition of Cic.name * Cic.term
 ;;
 
 type metasenv = (int * Cic.term) list;;
 
-type context = (binder_type * Cic.name * Cic.term) list;;
+type named_context = binder_type list;;
 
-type sequent = context * Cic.term;;
+type sequent = named_context * Cic.term;;
 
 let proof =
  ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
@@ -20,12 +20,11 @@ let goal = ref (None : (int * sequent) option);;
 
 exception NotImplemented
 
-(*CSC: Funzione che deve sparire!!! *)
-let cic_context_of_context =
+let cic_context_of_named_context =
  List.map
   (function
-      Declaration,_,t -> t
-    | Definition,_,_ -> raise NotImplemented
+      Declaration (_,t) -> Cic.Decl t
+    | Definition (_,t) -> Cic.Def t
   )
 ;;
 
@@ -192,10 +191,10 @@ let intros () =
 (*CSC: generatore di nomi? Chiedere il nome? *)
             | C.Anonimous -> C.Name "fresh_name"
           in
-           ((Declaration,n',s)::ctx,ty,C.Lambda(n',s,bo))
+           ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
       | C.LetIn (n,s,t) ->
          let (ctx,ty,bo) = collect_context t in
-          ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
+          ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
       | _ as t -> [], t, (C.Meta newmeta)
     in
      let revcontext',ty',bo' = collect_context ty in
@@ -221,8 +220,7 @@ let exact bo =
        (* Invariant: context is the actual context of the meta in the proof *)
        metano,context,ty
   in
-   (*CSC: deve sparire! *)
-   let context = cic_context_of_context context in
+   let context = cic_context_of_named_context context in
     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
      begin
       refine_meta metano bo [] ;
@@ -321,8 +319,7 @@ let apply term =
        (* Invariant: context is the actual context of the meta in the proof *)
        metano,context,ty
   in
-   (*CSC: deve sparire! *)
-   let ciccontext = cic_context_of_context context in
+   let ciccontext = cic_context_of_named_context context in
     let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
      let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in
       let bo' =
@@ -407,8 +404,7 @@ let elim term =
        (* Invariant: context is the actual context of the meta in the proof *)
        metano,context,ty
   in
-   (*CSC: deve sparire! *)
-   let ciccontext = cic_context_of_context context in
+   let ciccontext = cic_context_of_named_context context in
     let termty = T.type_of_aux' metasenv ciccontext term in
     let uri,cookingno,typeno,args =
      match termty with
@@ -562,7 +558,13 @@ let reduction_tactic reduction_function term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
     let ty' = replace ty in
-    let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+    let context' =
+     List.map
+      (function
+          Definition  (n,t) -> Definition  (n,replace t)
+        | Declaration (n,t) -> Declaration (n,replace t)
+      ) context
+    in
      let metasenv' = 
       List.map
        (function
@@ -618,7 +620,13 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
     let ty' = replace ty in
-    let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+    let context' =
+     List.map
+      (function
+          Declaration (n,t) -> Declaration (n,replace t)
+        | Definition  (n,t) -> Definition (n,replace t)
+      ) context
+    in
      let metasenv' = 
       List.map
        (function
@@ -654,10 +662,34 @@ prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
      refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
      goal :=
       Some
-       (newmeta1,((Declaration, C.Name "dummy_for_cut", term)::context,
+       (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
         newmeta1ty))
 ;;
 
+let letin term =
+ let module C = Cic in
+  let curi,metasenv,pbo,pty =
+   match !proof with
+      None -> assert false
+    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+  in
+  let (metano,context,ty) =
+   match !goal with
+      None -> assert false
+    | Some (metano,(context,ty)) -> metano,context,ty
+  in
+   let ciccontext = cic_context_of_named_context context in
+   let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
+    let newmeta = new_meta () in
+     let newmetaty = CicSubstitution.lift 1 ty in
+     let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
+      refine_meta metano bo' [newmeta,newmetaty];
+      goal :=
+       Some
+        (newmeta,
+         ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
+;;
+
 exception NotConvertible;;
 
 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
@@ -675,8 +707,7 @@ let change ~goal_input ~input =
      None -> assert false
    | Some (metano,(context,ty)) -> metano,context,ty
  in
-  (*CSC: deve sparire! *)
-  let ciccontext = cic_context_of_context context in
+  let ciccontext = cic_context_of_named_context context in
    (* are_convertible works only on well-typed terms *)
    ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
    if CicReduction.are_convertible goal_input input then