]> matita.cs.unibo.it Git - helm.git/commitdiff
- metas_of_term moved to cicUtil
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 May 2006 12:19:04 +0000 (12:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 May 2006 12:19:04 +0000 (12:19 +0000)
- fixed proof generation
- added again typechecking of generated proof

helm/software/components/binaries/tptp2grafite/main.ml
helm/software/components/cic/cicUtil.ml
helm/software/components/cic/cicUtil.mli
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/utils.ml

index 315bfc1006b94175f94a94f0af3e8ac85dd8d9f4..18fa713a9a05b1f48b71ae81528652018ce28453 100644 (file)
@@ -151,7 +151,7 @@ let convert_ast statements context = function
           statements, f::context
       | A.Negated_conjecture ->
           if collect_fv_from_formulae f <> [] then
-            (*prerr_endline "CONTIENE FV";*)();
+            prerr_endline "CONTIENE FV";
           let f = 
             PT.Binder 
              (`Forall,
index 7c6e3eabe28619cc14fdd0cb812f998566d38b52..51d84392bfaff40f8932ac8b8b471dd191c9cdf3 100644 (file)
@@ -363,3 +363,29 @@ let rehash_obj =
      in
      C.InductiveDefinition (tl', params', paramsno, attrs)
 
+let rec metas_of_term = function
+  | Cic.Meta (i, c) -> [i,c]
+  | Cic.Var (_, ens) 
+  | Cic.Const (_, ens) 
+  | Cic.MutInd (_, _, ens) 
+  | Cic.MutConstruct (_, _, _, ens) ->
+      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+  | Cic.Cast (s, t)
+  | Cic.Prod (_, s, t)
+  | Cic.Lambda (_, s, t)
+  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+  | Cic.MutCase (uri, i, s, t, l) ->
+      (metas_of_term s) @ (metas_of_term t) @
+        (List.flatten (List.map metas_of_term l))
+  | Cic.Fix (i, il) ->
+      List.flatten
+        (List.map (fun (s, i, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | Cic.CoFix (i, il) ->
+      List.flatten
+        (List.map (fun (s, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | _ -> []
+;;      
+
index b6fd7459dea6176bbf931a2c4e513c4fffc54472..4391efc821ec6d0e2fe318e38c0faeb1aa9af48d 100644 (file)
@@ -35,6 +35,7 @@ val clean_up_local_context :
 
 val is_closed : Cic.term -> bool
 val is_meta_closed : Cic.term -> bool
+val metas_of_term : Cic.term -> (int * Cic.term option list) list
 
   (** @raise Failure "not enough prods" *)
 val strip_prods: int -> Cic.term -> Cic.term
index 34b69718f50413569c247ce90d7d443a44240017..521c7635c09f850c0363cb1c2cccffe491f43f69 100644 (file)
@@ -468,14 +468,18 @@ let pp_proof names goalproof proof =
 let build_goal_proof l initial ty se =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let proof,se = 
-   List.fold_left 
-   (fun (current_proof,se) (pos,id,subst,pred) -> 
-      let p,l,r = proof_of_id id in
-      let p = build_proof_term p in
-      let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
-        build_proof_step subst current_proof p pos l r pred,
-        List.map (fun x -> Subst.apply_subst subst x) se)
-   (initial,se) l
+    let rec aux se current_proof = function
+      | [] -> current_proof,se
+      | (pos,id,subst,pred)::tl ->
+           let p,l,r = proof_of_id id in
+           let p = build_proof_term p in
+           let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+           let proof = build_proof_step subst current_proof p pos l r pred in
+           let proof,se = aux se proof tl in
+           Subst.apply_subst subst proof,
+           List.map (fun x -> Subst.apply_subst subst x) se
+    in
+    aux se initial l
   in
   canonical (contextualize_rewrites proof ty), se
 ;;
index b93f6b09195885db698ba6e053b40b1f1ea8695c..cfada50855c633a2f1532f1fb6cac2774282eef8 100644 (file)
@@ -1269,14 +1269,18 @@ let rec check goal = function
   
 let simplify_goal_set env goals passive active = 
   let active_goals, passive_goals = goals in 
+  let find (_,_,g) where =
+    List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
+  in
   let simplified =
-    HExtlib.filter_map 
-      (fun g -> 
+    List.fold_left
+      (fun acc g -> 
         match simplify_goal env g ~passive active with 
-        | true, g -> Some g
-        | false, g -> Some g)
-      active_goals
+        | _, g -> if find g acc then acc else g::acc)
+      [] active_goals
   in
+  if List.length active_goals <>  List.length simplified then
+    prerr_endline "SEMPLIFICANDO HO SCARTATO...";
   (simplified,passive_goals)
         (*
   HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
@@ -1300,13 +1304,20 @@ let check_if_goals_set_is_solved env active goals =
 
 let infer_goal_set env active goals = 
   let active_goals, passive_goals = goals in
-  match passive_goals with
-  | [] -> goals
-  | hd::tl -> 
-      let selected = hd in
-      let passive_goals = tl in
-      let new' = Indexing.superposition_left env (snd active) selected in
-      selected::active_goals, passive_goals @ new'
+  let rec aux = function
+    | [] -> goals
+    | ((_,_,t1) as hd)::tl when 
+       not (List.exists 
+             (fun (_,_,t) -> Equality.meta_convertibility t t1) 
+             active_goals)
+       -> 
+        let selected = hd in
+        let passive_goals = tl in
+        let new' = Indexing.superposition_left env (snd active) selected in
+        selected::active_goals, passive_goals @ new'
+    | _::tl -> aux tl
+  in 
+  aux passive_goals
 ;;
 
 let infer_goal_set_with_current env current goals = 
@@ -1791,6 +1802,7 @@ let saturate
       let goal_proof = replace goal_proof in
         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste? 
          * what mi pare buono, sostituisce solo le meta farlocche *)
+        prerr_endline (CicPp.pp goal_proof names);
       let side_effects_t = List.map replace side_effects_t in
       (* check/refine/... build the new proof *)
       let replaced_goal = 
@@ -1813,10 +1825,16 @@ let saturate
         | CicUnification.AssertFailure s -> 
             fail "Maybe the local context of metas in the goal was not an IRL" s
       in
-      
       let final_subst = 
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
+      let _ = 
+        let ty,_ =
+          CicTypeChecker.type_of_aux' real_menv context goal_proof
+            CicUniv.empty_ugraph
+        in
+        ty
+      in
       let proof, real_metasenv = 
         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
           proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
index 6a32e25953f5afff5df75c0ce55058c246303a0c..072d64f66cd76b785c2585d7469b014739d1fd40 100644 (file)
@@ -733,29 +733,7 @@ let eq_XURI () =
   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
 let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
 
-let rec metas_of_term = function
-  | Cic.Meta (i, c) -> [i]
-  | Cic.Var (_, ens) 
-  | Cic.Const (_, ens) 
-  | Cic.MutInd (_, _, ens) 
-  | Cic.MutConstruct (_, _, _, ens) ->
-      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
-  | Cic.Cast (s, t)
-  | Cic.Prod (_, s, t)
-  | Cic.Lambda (_, s, t)
-  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
-  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
-  | Cic.MutCase (uri, i, s, t, l) ->
-      (metas_of_term s) @ (metas_of_term t) @
-        (List.flatten (List.map metas_of_term l))
-  | Cic.Fix (i, il) ->
-      List.flatten
-        (List.map (fun (s, i, t1, t2) ->
-                     (metas_of_term t1) @ (metas_of_term t2)) il)
-  | Cic.CoFix (i, il) ->
-      List.flatten
-        (List.map (fun (s, t1, t2) ->
-                     (metas_of_term t1) @ (metas_of_term t2)) il)
-  | _ -> []
-;;      
+let metas_of_term t = 
+  List.map fst (CicUtil.metas_of_term t)
+;;