]> matita.cs.unibo.it Git - helm.git/commitdiff
new more flexible compose, see matita/tests/compose.ma for a sample
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Jun 2007 12:20:18 +0000 (12:20 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Jun 2007 12:20:18 +0000 (12:20 +0000)
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/compose.ml
helm/software/components/tactics/compose.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/Makefile
helm/software/matita/tests/compose.ma [new file with mode: 0644]

index 9a453ae42d196f2ddc844e5d5856d82035ca2737..0b54b68a4c6a1717b5d515f976cb2f40ce65be79 100644 (file)
@@ -65,7 +65,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident list
   | ClearBody of loc * 'ident
-  | Compose of loc * 'term * 'term * 'ident intros_spec
+  | Compose of loc * 'term * 'term option * int * 'ident intros_spec
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
index 51b002de9b8d2910734cf0a2d65a73ac30ad896a..f689ff101d1c78561248b32c1a64dd7adeddde71 100644 (file)
@@ -107,8 +107,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)
   | ClearBody (_,id) -> Printf.sprintf "clearbody %s" (pp_hyps [id])
   | Constructor (_,n) -> "constructor " ^ string_of_int n
-  | Compose (_,t1, t2, intro_specs) -> 
-      Printf.sprintf "compose %s %s%s" (term_pp t1) (term_pp t1)
+  | Compose (_,t1, t2, times, intro_specs) -> 
+      Printf.sprintf "compose %s%s %s%s" 
+        (if times > 0 then string_of_int times ^ " " else "")
+        (term_pp t1) (match t2 with None -> "" | Some t2 -> "with "^term_pp t2)
         (pp_intros_specs " as " intro_specs)
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
index 6b34c687ccf38fcf13c168c67c3d786e066860d5..ad4ae40c6c6d2e7f040e9ed82ec892d37db01cc6 100644 (file)
@@ -96,8 +96,8 @@ let rec tactic_of_ast status ast =
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
-  | GrafiteAst.Compose (_,t1,t2,(howmany, names)) -> 
-      Tactics.compose t1 t2 ?howmany
+  | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> 
+      Tactics.compose times t1 t2 ?howmany
         ~mk_fresh_name_callback:(namer_of names)
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
index 31b881988076b4c46a72adbbb0ee9a64fc798c9b..ececcf967934f82ee5ccbbeb150b07b85e405b15 100644 (file)
@@ -195,10 +195,16 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
-    | GrafiteAst.Compose (loc, t1, t2, spec) ->
+    | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
         let metasenv,t1 = disambiguate_term context metasenv t1 in
-        let metasenv,t2 = disambiguate_term context metasenv t2 in
-        metasenv,   GrafiteAst.Compose (loc, t1, t2, spec)
+        let metasenv,t2 = 
+          match t2 with
+          | None -> metasenv, None
+          | Some t2 -> 
+              let m, t2 = disambiguate_term context metasenv t2 in
+              m, Some t2
+        in
+        metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
index 10a841e2eae14e01db81a03147ca3ace7ebb8bfe..45a71f174dea678322b79bd97fcaecf0e5a31b79 100644 (file)
@@ -156,9 +156,10 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
-      specs = intros_spec ->
-        GrafiteAst.Compose (loc, t1, t2, specs)
+    | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
+      OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
+        let times = match times with None -> 1 | Some i -> i in
+        GrafiteAst.Compose (loc, t1, t2, times, specs)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
index 4f1d1b182159eb334710bff22b2caa8a57d1e139..3e64110987cef40500d3339e833f007204525f55 100644 (file)
@@ -78,6 +78,7 @@ exception UnableToCompose
  * both living in the same context and metasenv *)
 let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   let module RT = RefinementTool in
+  let original_metasenv = metasenv in 
   let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
   let rec mk_implicits = function
@@ -177,8 +178,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
     List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
           try List.assoc i meta2no -  List.assoc j meta2no 
-          with Not_found -> 
-            assert false) 
+          with Not_found -> assert false) 
       body_metasenv
   in
   let namer l n = 
@@ -221,6 +221,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
       debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
       let term = CicMetaSubst.apply_subst subst term in
+      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
       debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
       let term, ty, metasenv, ugraph = 
         CicRefine.type_of_aux' metasenv context term ugraph
@@ -229,6 +230,15 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
         split_metasenv metasenv (spline_len + List.length context)
       in
       let term = purge_unused_lambdas lambdas_metasenv term in
+      let metasenv = 
+        List.filter 
+          (fun (i,_,_) -> 
+            List.for_all 
+              (fun (j,_,_) ->
+                i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv) 
+              lambdas_metasenv) 
+          metasenv 
+      in
       debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
       debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       term, metasenv, ugraph
index f090c3dbfeb6504f15c7136ef505f414cc61df62..137e919b09fd98e6c5d6da3f5f155cd79b7850c6 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) =
+let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 ;;
+
+let compose_core t2 t1 (proof, goal) =
   let _,metasenv,_subst,_,_,_ = proof in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
   let ty1,_ = 
     CicTypeChecker.type_of_aux' metasenv context t1 CicUniv.oblivion_ugraph 
   in
-  let rec count_pi = function Cic.Prod (_,_,t) -> count_pi t + 1 | _ -> 0 in
-  let rec generate arity menv acc =
-    if arity < 0 then acc, menv
-    else
+  let ty2,_ = 
+    CicTypeChecker.type_of_aux' metasenv context t2 CicUniv.oblivion_ugraph 
+  in
+  let saturated_ty2, menv_for_saturated_ty2 = 
+    let maxm = CicMkImplicit.new_meta metasenv [] in
+    let ty2, menv, _, _ = TermUtil.saturate_term maxm metasenv context ty2 0 in
+    ty2, menv
+  in
+  (* unifies t with saturated_ty2 and gives back a fresh meta of type t *)
+  let unif menv t = 
+    let m, menv2 =
+      let n = CicMkImplicit.new_meta menv [] in
+      let irl = 
+        CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+      Cic.Meta (n,irl), ((n,context,t)::menv)
+    in
+    try 
+      let _ = 
+        CicUnification.fo_unif menv context t saturated_ty2
+          CicUniv.oblivion_ugraph
+      in 
+        true, menv2, m
+    with
+    | CicUnification.UnificationFailure _
+    | CicUnification.Uncertain _ -> false, menv2, m
+  in
+  (* check which "positions" in the input arrow unifies with saturated_ty2 *)
+  let rec positions menv cur arity = function 
+    | Cic.Prod (n,s,t) -> 
+        let b, newmenv, sb = unif menv s in
+        if b then
+          (arity - cur - 1) :: 
+            (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t))
+        else
+          positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)
+    | _ -> []
+  in
+  (* position is a list of arities, that is if t1 : a -> b -> c and arity is
+   * 0 then the computed term will be (t1 ? t2) of type a -> c
+   * if arity is 1 then (t1 t2 ?) of type b -> c *)
+  let rec generate positions menv acc =
+    match positions with
+    | [] -> acc, menv
+    | arity::tl ->
       try
-        let t, menv, _ =
-          CloseCoercionGraph.generate_composite t1 t2 context menv
+        let t, menv1, _ =
+          CloseCoercionGraph.generate_composite t2 t1 context menv
             CicUniv.oblivion_ugraph arity false
         in
-        generate (arity - 1) menv (t::acc)
+        assert (List.length menv1 = List.length menv);
+        generate tl menv (t::acc)
       with 
-      | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc
+      | CloseCoercionGraph.UnableToCompose -> generate tl menv acc
+  in
+  let terms, metasenv =
+    generate (positions menv_for_saturated_ty2 0 (count_pi ty1) ty1) metasenv []
   in
-  let terms, metasenv = generate (count_pi ty1) metasenv [] in
+  (* the new proof has the resulting metasenv (shouldn't it be the same?) *)
   let proof = 
     let uri, _, _subst, bo, ty, attrs = proof in
     uri, metasenv, _subst, bo, ty, attrs
   in
+  (* now we have the terms, we generalize them and intros them *)
   let proof, goal =
     List.fold_left 
       (fun (proof,goal) t ->
@@ -62,12 +110,64 @@ let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (proof, goal) =
         proof,List.hd gl)
       (proof,goal) terms
   in
-  ProofEngineTypes.apply_tactic 
-    (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
-    (proof,goal)
+  (proof, goal), List.length terms
+;;
+
+let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
+  let ((proof, goal), k), n = 
+    match t2 with
+    | Some t2 -> compose_core t1 t2 proofstatus, n-1
+    | None -> 
+        let k = 
+          let proof, goal = proofstatus in
+          let _,metasenv,subst,_,_,_ = proof in
+          let _,_,ty = CicUtil.lookup_meta goal metasenv in
+          count_pi (CicMetaSubst.apply_subst subst ty)
+        in
+        (proofstatus, k), n
+  in
+  let (proof, goal), k = 
+    (* fix iterates n times the composition *)
+    let rec fix proofstatus k t = function
+      | 0 -> proofstatus, k
+      | n ->
+          let t = CicSubstitution.lift k t in
+          let proof, gl =  
+            ProofEngineTypes.apply_tactic 
+              (PrimitiveTactics.intros_tac 
+                ~howmany:k ?mk_fresh_name_callback ()) proofstatus
+          in
+          assert (List.length gl = 1);
+          let goal = List.hd gl in
+          let k, proofstatus =
+            (* aux compose t with every previous result *)
+            let rec aux k proofstatus = function
+              | 0 -> k, proofstatus
+              | n -> 
+                 let (proof, goal), k1 = 
+                   compose_core t (Cic.Rel n) proofstatus 
+                 in
+                 aux (k+k1) (proof, goal) (n-1)
+            in
+              aux 0 (proof, goal) k
+          in
+          fix proofstatus k t (n-1)
+    in
+      fix (proof, goal) k t1 n
+  in
+  let howmany = 
+    match howmany with
+    | None -> None
+    | Some i ->
+        if i - k < 0 then (* we should generalize back and clear *) Some 0
+        else Some (i - k)
+  in
+     ProofEngineTypes.apply_tactic 
+      (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
+      (proof,goal)
 ;;
 
-let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 =
+let compose_tac ?howmany ?mk_fresh_name_callback times t1 t2 =
   ProofEngineTypes.mk_tactic 
-    (compose_tac ?howmany ?mk_fresh_name_callback t1 t2)
+    (compose_tac ?howmany ?mk_fresh_name_callback times t1 t2)
 ;;
index 37e69d42f3f37dfd9c78fd7d5b318b42f1fa9bb7..44db74b76aa2fe3ecb134d1be46e6d9311f57fb2 100644 (file)
@@ -26,4 +26,5 @@
 val compose_tac: 
   ?howmany:int -> 
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  int (* times *) ->
+  Cic.term -> Cic.term option -> ProofEngineTypes.tactic
index d63e8805cf6d846e92b63d16e4c74cd236c9a9ce..16c668266987e31378f64737531ba32c16ba2017 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun  1 17:03:59 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Jun  4 13:44:18 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -105,4 +105,4 @@ val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val compose :
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> Cic.term -> ProofEngineTypes.tactic
+  int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic
index 81e67db6447e3e51e84e7dfb44394c5d69115865..1e940c3b8c5218aa1e8d5dc8c43d4ad028d398b0 100644 (file)
@@ -86,11 +86,6 @@ CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
 MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
 $(CMOS) : $(LIB_DEPS)
 $(CMXOS): $(LIBX_DEPS)
-ifeq ($(MAKECMDGOALS),opt)
-       $(MLI:%.mli=%.cmi): $(LIBX_DEPS)
-else
-        $(MLI:%.mli=%.cmi): $(LIB_DEPS)
-endif
 
 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
@@ -404,21 +399,31 @@ depend.opt:
        $(H)echo "  OCAMLDEP -native"
        $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt
 
-ifeq ($(MAKECMDGOALS),)
-  include .depend   
-endif
-
-ifeq ($(MAKECMDGOALS), all)
-  include .depend   
+# this should be sligtly better, since should work with 'make all opt'
+ifneq (,$(findstring all,$(MAKECMDGOALS)))
+  # if we 'make all opt' the deps for 'all' should be fine also for opt
+       # if we 'make opt all' it should not work...
+  TO_INCLUDE+=.depend
+  TO_DEPEND_ON=$(LIB_DEPS)
+else ifneq (,$(findstring opt,$(MAKECMDGOALS)))
+  TO_INCLUDE+=.depend.opt
+  TO_DEPEND_ON=$(LIBX_DEPS)
+else ifneq (,$(findstring world,$(MAKECMDGOALS)))
+  ifeq ($(HAVE_OCAMLOPT),yes)
+    TO_INCLUDE+=.depend.opt
+    TO_DEPEND_ON=$(LIBX_DEPS)
+  else
+    TO_INCLUDE+=.depend
+    TO_DEPEND_ON=$(LIB_DEPS)
+  endif
+else
+  TO_INCLUDE+=.depend
+  TO_DEPEND_ON=$(LIB_DEPS)
 endif
 
-ifeq ($(MAKECMDGOALS), opt)
-  include .depend.opt   
-endif
+$(MLI:%.mli=%.cmi): $(TO_DEPEND_ON)
 
-ifeq ($(MAKECMDGOALS), world)
-  include .depend.opt   
-endif
+include $(TO_INCLUDE)
 
 %.cmi: %.mli
        $(H)echo "  OCAMLC $<"
diff --git a/helm/software/matita/tests/compose.ma b/helm/software/matita/tests/compose.ma
new file mode 100644 (file)
index 0000000..5d60357
--- /dev/null
@@ -0,0 +1,53 @@
+set "baseuri" "cic:/matita/tests/compose/LCL002-1".
+include "logic/equality.ma".
+
+theorem an_1:
+∀ Univ:Set.
+∀ a:Univ.
+∀ is_a_theorem:Univ → Prop.
+∀ not:Univ → Univ.
+∀ or:Univ → Univ → Univ.
+∀ H0:∀ U:Univ.∀ V:Univ.∀ X:Univ.∀ Y:Univ.∀ Z:Univ.
+  is_a_theorem 
+    (or (not (or (not (or (not X) Y)) (or Z (or U V)))) 
+        (or (not (or (not U) X)) (or Z (or V X)))).
+∀ H1:∀ X:Univ.∀ Y:Univ.
+  is_a_theorem (or (not X) Y) → is_a_theorem X → is_a_theorem Y.
+∀ ABS:∀ X.is_a_theorem X.
+True.
+.
+intros 5.
+intros (H H1 ABS).
+
+(* H1 o H *)
+compose (H) with (H1) (primo secondo).
+letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H ? ? ? ? ?)); 
+try assumption; [1,2: apply ABS]
+letin verifica_secondo ≝ (secondo ? ? ? ? ? ? ? = H1 ? ? (H ? ? ? ? ?) ?);
+try assumption; [1,2: apply ABS]
+clear verifica_primo verifica_secondo.
+compose (H) with (primo) (terzo).
+compose (H) with (secondo) (quarto).
+letin verifica_terzo_quarto ≝ (terzo ? ? ? ? ? = quarto ? ? ? ? ?);
+try assumption.
+clear verifica_terzo_quarto.
+clear primo secondo terzo quarto.
+
+(* H1 o H1 *)
+compose (H1) with (H1) (primo secondo).
+letin verifica_primo ≝ (primo ? ? ? ? ? ? = H1 ? ? ? (H1 ? ? ? ?));
+try assumption; [1,2,3,4,5,6: apply ABS]
+letin verifica_secondo ≝ (secondo ? ? ? ? ? ? = H1 ? ? (H1 ? ? ? ?) ?);
+try assumption; [1,2,3,4,5,6: apply ABS]
+clear verifica_primo verifica_secondo.
+clear primo secondo.
+
+(* close H1 o H1 with H *)
+compose H1 with H1 0. 
+(* 
+leaving the result under the sequent line and calling compose without 
+the with parameter, will compose H with all the stuff under the sequent line
+*)
+compose 3 (H) (i1 i2 p1 p2 p3 p4 p5 p6 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12).
+exact I.
+qed.