parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index 7d223a4437b4d9fe232032315b9ec8c933a17a6a..d95d37d8ca53090771a8f10a7f1068d0eb0f3677 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -27,8 +27,8 @@
 
 exception Bad_pattern of string Lazy.t
 
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
-  CicMkImplicit.new_meta metasenv []
+let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
+  CicMkImplicit.new_meta metasenv subst
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,initial_subst,bo,ty, attrs = proof in
@@ -56,7 +56,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
          i,canonical_context',(subst_in ty)
       ) metasenv'
     in
-     let bo' = subst_in bo in
+     let bo' = lazy (subst_in (Lazy.force bo)) in
      (* Metavariables can appear also in the *statement* of the theorem
       * since the parser does not reject as statements terms with
       * metavariable therein *)
@@ -79,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
  let (uri,_,initial_subst,bo,ty, attrs) = proof in
   let subst_in = CicMetaSubst.apply_subst subst in
-  let bo' = subst_in bo in
+  let bo' = lazy (subst_in (Lazy.force bo)) in
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
    * metavariable therein *)
@@ -229,7 +229,9 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
   in
   find subst metasenv ugraph context wanted t
   
-let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
+let select_in_term 
+  ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where) 
+=
   let add_ctx context name entry = (Some (name, entry)) :: context in
   let map2 error_msg f l1 l2 = 
     try 
@@ -313,13 +315,13 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
      | Some where -> aux context where term
    in
     match wanted with
-       None -> [],metasenv,ugraph,roots
+       None -> subst,metasenv,ugraph,roots
      | Some wanted ->
-        let rec find_in_roots =
+        let rec find_in_roots subst =
          function
-            [] -> [],metasenv,ugraph,[]
+            [] -> subst,metasenv,ugraph,[]
           | (context',where)::tl ->
-             let subst,metasenv,ugraph,tl' = find_in_roots tl in
+             let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
              let subst,metasenv,ugraph,found =
               let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
                find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
@@ -327,7 +329,8 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
              in
               subst,metasenv,ugraph,found @ tl'
         in
-         find_in_roots roots
+         find_in_roots subst roots
+;;
 
 (** create a pattern from a term and a list of subterms.
 * the pattern is granted to have a ? for every subterm that has no selected
@@ -483,7 +486,7 @@ exception Fail of string Lazy.t
   *
   * @raise Bad_pattern
   * *)
-  let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
+  let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty)
        ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
   =
    let what, hyp_patterns, goal_pattern = pattern in
@@ -507,8 +510,9 @@ exception Fail of string Lazy.t
      aux [] context
    in
    let subst,metasenv,ugraph,ty_terms =
-    select_in_term ~metasenv ~context ~ugraph ~term:ty
-     ~pattern:(what,goal_pattern) in
+    select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty
+     ~pattern:(what,goal_pattern) 
+   in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
@@ -521,7 +525,7 @@ exception Fail of string Lazy.t
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
                 let subst,metasenv,ugraph,terms =
-                 select_in_term ~metasenv ~context ~ugraph ~term
+                 select_in_term ~subst ~metasenv ~context ~ugraph ~term
                   ~pattern:(what, Some pat)
                 in
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
@@ -534,11 +538,11 @@ exception Fail of string Lazy.t
                  (entry::context)
             | Some pat -> 
                 let subst,metasenv,ugraph,terms_bo =
-                 select_in_term ~metasenv ~context ~ugraph ~term:bo
+                 select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo
                   ~pattern:(what, Some pat) in
                 let subst,metasenv,ugraph,terms_ty =
                  let subst,metasenv,ugraph,res =
-                  select_in_term ~metasenv ~context ~ugraph ~term:ty
+                  select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty
                    ~pattern:(what, Some pat)
                  in
                   subst,metasenv,ugraph,res
@@ -550,6 +554,7 @@ exception Fail of string Lazy.t
      subst,metasenv,ugraph,res
    in
     subst,metasenv,ugraph,context_terms, ty_terms
+;;
 
 (** locate_in_term equality what where context
 * [what] must match a subterm of [where] according to [equality]
@@ -640,6 +645,32 @@ let lookup_type metasenv context hyp =
    in
    aux 1 context
 
+let find_hyp name =
+ let rec find_hyp n =
+  function
+     [] -> assert false
+   | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+      Cic.Rel n, CicSubstitution.lift n ty
+   | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+   | _::tl -> find_hyp (n+1) tl
+ in
+  find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+  List.sort
+   (fun (id1,_) (id2,_) ->
+     let t1,_ = find_hyp id1 context in
+     let t2,_ = find_hyp id2 context in
+     match t1,t2 with
+        Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+      | _,_ -> assert false) hpatterns
+ in
+  t,hpatterns,cpattern
+;;
+
 (* FG: **********************************************************************)
 
 let get_name context index =