]> matita.cs.unibo.it Git - helm.git/commitdiff
new compose tactic, still undocumented.
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)
moved from library to tactics the code for composing coercions.

17 files changed:
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/library/cicCoercion.ml
components/library/cicCoercion.mli
components/tactics/.depend
components/tactics/.depend.opt
components/tactics/Makefile
components/tactics/closeCoercionGraph.ml [new file with mode: 0644]
components/tactics/closeCoercionGraph.mli [new file with mode: 0644]
components/tactics/compose.ml [new file with mode: 0644]
components/tactics/compose.mli [new file with mode: 0644]
components/tactics/tactics.ml
components/tactics/tactics.mli
matita/matita.lang

index 2dc077f063ffb125125795b091a9fc91f7c52dce..9a453ae42d196f2ddc844e5d5856d82035ca2737 100644 (file)
@@ -65,6 +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
   | Constructor of loc * int
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
index 811da9ddce9e7fe6058381969c9149b09f5a1f9e..51b002de9b8d2910734cf0a2d65a73ac30ad896a 100644 (file)
@@ -107,6 +107,9 @@ 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)
+        (pp_intros_specs " as " intro_specs)
   | Contradiction _ -> "contradiction"
   | Cut (_, ident, term) ->
      "cut " ^ term_pp term ^
index 97be9ab2dc08ca4bca2b897a45d6cae930b85219..6b34c687ccf38fcf13c168c67c3d786e066860d5 100644 (file)
@@ -96,6 +96,9 @@ 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
+        ~mk_fresh_name_callback:(namer_of names)
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
index d52b0e2de830105c80ee5837fe5902e583b2edc4..31b881988076b4c46a72adbbb0ee9a64fc798c9b 100644 (file)
@@ -195,6 +195,10 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
+    | GrafiteAst.Compose (loc, t1, t2, 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)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
index 17144a85244a40cea868499ac3ce36c1fb535059..10a841e2eae14e01db81a03147ca3ace7ebb8bfe 100644 (file)
@@ -149,13 +149,16 @@ EXTEND
         GrafiteAst.AutoBatch (loc,params)
     | IDENT "cases"; what = tactic_term;
       specs = intros_spec ->
-       GrafiteAst.Cases (loc, what, specs)
+        GrafiteAst.Cases (loc, what, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
         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 "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
index 6f2443e98a45798f511279a0c5dd74e0a7e5bd07..fe1c961fb3c8dd7791250ee97e783b56fa30584f 100644 (file)
 
 (* $Id$ *)
 
-let debug = false
-let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
-
-(* given the new coercion uri from src to tgt returns the list 
- * of new coercions to create. hte list elements are
- * (source, list of coercions to follow, target)
- *)
-let get_closure_coercions src tgt uri coercions =
-  let eq_carr s t = 
-    try
-      CoercDb.eq_carr s t
-    with
-    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
-  in
-  match src,tgt with
-  | CoercDb.Uri _, CoercDb.Uri _ ->
-      let c_from_tgt = 
-        List.filter 
-          (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
-          coercions 
-      in
-      let c_to_src = 
-        List.filter 
-          (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
-          coercions 
-      in
-        (HExtlib.flatten_map 
-          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
-        (HExtlib.flatten_map 
-          (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
-        (HExtlib.flatten_map 
-          (fun (s,_,u1l) ->
-            HExtlib.flatten_map 
-              (fun (_,t,u2l) ->
-                HExtlib.flatten_map
-                  (fun u1 ->
-                    List.map 
-                      (fun u2 -> (s,[u1;uri;u2],t)) 
-                      u2l)
-                  u1l) 
-              c_from_tgt) 
-          c_to_src)
-  | _ -> [] (* do not close in case source or target is not an indty ?? *)
-;;
-
-let obj_attrs n = [`Class (`Coercion n); `Generated]
-
-exception UnableToCompose
-
-(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure rt c1 c2 univ arity =
-  let module RT = RefinementTool in
-  let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
-  let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
-  let rec mk_implicits = function
-    | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
-  in
-  let rec mk_lambda_spline c namer = function
-    | 0 -> c
-    | n -> 
-        Cic.Lambda 
-          (namer n,
-           (Cic.Implicit None), 
-           mk_lambda_spline c namer (n-1))
-  in 
-  let count_saturations_needed t arity = 
-    let rec aux acc n = function
-      | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> 
-          aux (acc@[name]) (n+1) t
-      | _ -> n,acc
-    in
-    let len,names = aux [] 0 t in
-    let len = len - arity in
-    List.fold_left 
-      (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) 
-      names
-  in
-  let compose c1 nc1 c2 nc2 =
-    Cic.Lambda 
-      (Cic.Name "x",
-      (Cic.Implicit None),
-      Cic.Appl ( c2 :: mk_implicits nc2 @ 
-        [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
-  in
-(*
-  let order_metasenv metasenv = 
-    let module OT = struct type t = int let compare = Pervasives.compare end in
-    let module S = HTopoSort.Make (OT) in
-    let dep i = 
-      let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
-      let metas = List.map fst (CicUtil.metas_of_term ty) in
-      HExtlib.list_uniq (List.sort Pervasives.compare metas)
-    in
-    let om =  
-      S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep 
-    in
-    List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
-  in 
-*)
-  let rec create_subst_from_metas_to_rels n = function 
-    | [] -> []
-    | (metano, ctx, ty)::tl -> 
-        (metano,(ctx,Cic.Rel (n+1),ty)) ::
-          create_subst_from_metas_to_rels (n-1) tl
-  in
-  let split_metasenv metasenv n =
-    List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
-  in
-  let purge_unused_lambdas metasenv t =
-    let rec aux = function
-        | Cic.Lambda (_, Cic.Meta (i,_), t) when  
-          List.exists (fun (j,_,_) -> j = i) metasenv ->
-            aux (CicSubstitution.subst (Cic.Rel ~-100) t)
-        | Cic.Lambda (name, s, t) -> 
-            Cic.Lambda (name, s, aux t)
-        | t -> t
-    in
-    aux t
-  in
-  let order_body_menv term body_metasenv =
-    let rec purge_lambdas = function
-      | Cic.Lambda (_,_,t) -> purge_lambdas t
-      | t -> t
-    in
-    let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
-    let metas_that_saturate l =
-      List.fold_left 
-        (fun (acc,n) t ->
-          let metas = CicUtil.metas_of_term t in
-          let metas = List.map fst metas in
-          let metas = 
-            List.filter 
-              (fun i -> List.for_all (fun (j,_) -> j<>i) acc) 
-              metas 
-          in
-          let metas = List.map (fun i -> i,n) metas in
-          metas @ acc, n+1)
-        ([],0) l
-    in
-    let l_c2 = skip_appl (purge_lambdas term) in
-    let l_c1 = 
-      match HExtlib.list_last l_c2 with
-      | Cic.Appl l -> List.tl l
-      | _ -> assert false
-    in
-    (* i should cut off the laet elem of l_c2 *)
-    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
-    List.sort 
-      (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
-          try List.assoc i meta2no -  List.assoc j meta2no 
-          with Not_found -> assert false) 
-      body_metasenv
-  in
-  let namer l n = 
-    let l = List.map (function Cic.Name s -> s | _ -> "A") l in
-    let l = List.fold_left
-      (fun acc s -> 
-        let rec add' s =
-          if List.exists ((=) s) acc then add' (s^"'") else s
-        in
-        acc@[add' s])
-      [] l
-    in
-    let l = List.rev l in 
-    Cic.Name (List.nth l (n-1))
-  in 
-  debug_print (lazy ("\nCOMPOSING"));
-  debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
-  debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
-  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
-  let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
-  let spline_len = saturations_for_c1 + saturations_for_c2 in
-  let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
-  debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
-  let c, univ = 
-    match rt.RT.type_of_aux' [] [] c univ with
-    | RT.Success (term, ty, metasenv, ugraph) -> 
-        debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
-(*         let metasenv = order_metasenv metasenv in *)
-(*         debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); *)
-        let body_metasenv, lambdas_metasenv = 
-          split_metasenv metasenv spline_len 
-        in
-(*
-        debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
-        debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
-*)
-        let body_metasenv = order_body_menv term body_metasenv in
-        debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
-        let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
-        debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst));
-        let term = rt.RT.apply_subst subst term in
-        debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
-        (match rt.RT.type_of_aux' metasenv [] term ugraph with
-        | RT.Success (term, ty, metasenv, ugraph) -> 
-            let body_metasenv, lambdas_metasenv = 
-              split_metasenv metasenv spline_len 
-            in
-            let term = purge_unused_lambdas lambdas_metasenv term in
-            debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
-            term, ugraph
-        | RT.Exception s -> debug_print s; raise UnableToCompose)
-    | RT.Exception s -> debug_print s; raise UnableToCompose
-  in  
-  let c_ty,univ = 
-    try 
-      CicTypeChecker.type_of_aux' [] [] c univ
-    with CicTypeChecker.TypeCheckerFailure s ->
-      debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) (Lazy.force s)));
-      raise UnableToCompose
-  in
-  let cleaned_ty =
-    FreshNamesGenerator.clean_dummy_dependent_types c_ty 
-  in
-  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in 
-    obj,univ
+let close_coercion_graph_ref = ref
+ (fun _ _ _ _ _ -> [] : 
+   RefinementTool.kit -> 
+   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+   string (* baseuri *) ->
+     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
 ;;
 
-(* removes from l the coercions that are in !coercions *)
-let filter_duplicates l coercions =
-  List.filter (
-      fun (src,l1,tgt) ->
-        not (List.exists (fun (s,t,l2) -> 
-          CoercDb.eq_carr s src && 
-          CoercDb.eq_carr t tgt &&
-          try 
-            List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
-          with
-          | Invalid_argument "List.for_all2" -> false)
-        coercions))
-  l
+let set_close_coercion_graph f = close_coercion_graph_ref := f;;
 
-let mangle s t l = 
-  (*List.fold_left
-    (fun s x -> s ^ "_" ^ x)
-    (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*)
-  s ^ "_OF_" ^ t
+let close_coercion_graph r c1 c2 u s = 
+  !close_coercion_graph_ref r c1 c2 u s
 ;;
-
-exception ManglingFailed of string 
-
-let number_if_already_defined buri name l =
-  let err () =
-    raise 
-      (ManglingFailed 
-        ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
-  in
-  let rec aux n =
-    let suffix = if n > 0 then string_of_int n else "" in
-    let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
-    let uri = UriManager.uri_of_string suri in
-    let retry () = 
-      if n < 100 then 
-        begin
-          HLog.warn ("Uri " ^ suri ^ " already exists.");
-          aux (n+1)
-        end
-      else
-        err ()
-    in
-    if List.exists (UriManager.eq uri) l then retry ()
-    else
-      try
-        let _  = Http_getter.resolve' ~writable:true uri in
-        if Http_getter.exists' uri then retry () else uri
-      with 
-      | Http_getter_types.Key_not_found _ -> uri
-      | Http_getter_types.Unresolvable_URI _ -> assert false
-  in
-  aux 0
-;;
-  
-(* given a new coercion uri from src to tgt returns 
- * a list of (new coercion uri, coercion obj, universe graph) 
- *)
-let close_coercion_graph rt src tgt uri baseuri =
-  (* check if the coercion already exists *)
-  let coercions = CoercDb.to_list () in
-  let todo_list = get_closure_coercions src tgt uri coercions in
-  let todo_list = filter_duplicates todo_list coercions in
-  try
-    let new_coercions = 
-      List.fold_left (
-        fun acc (src, l , tgt) ->
-          try 
-            (match l with
-            | [] -> assert false 
-            | he :: tl ->
-                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
-                let first_step = 
-                  Cic.Constant ("", 
-                    Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                    Cic.Sort Cic.Prop, [], obj_attrs arity)
-                in
-                let o,_ = 
-                  List.fold_left (fun (o,univ) coer ->
-                    match o with 
-                    | Cic.Constant (_,Some c,_,[],_) ->
-                        generate_composite_closure rt c 
-                          (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity
-                    | _ -> assert false 
-                  ) (first_step, CicUniv.empty_ugraph) tl
-                in
-                let name_src = CoercDb.name_of_carr src in
-                let name_tgt = CoercDb.name_of_carr tgt in
-                let by = List.map UriManager.name_of_uri l in
-                let name = mangle name_tgt name_src by in
-                let c_uri = 
-                  number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_) -> u) acc) 
-                in
-                let named_obj = 
-                  match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs) ->
-                      Cic.Constant (name,bo,ty,vl,attrs)
-                  | _ -> assert false 
-                in
-                  (src,tgt,c_uri,named_obj))::acc
-          with UnableToCompose -> acc
-      ) [] todo_list
-    in
-    new_coercions
-  with ManglingFailed s -> HLog.error s; []
-;;
-
index e3ee8dbfc8d46ed2418d1d988cc13da57d9a048e..789e7d00dff19a512230e84975f0b94c67b640b0 100644 (file)
 
 (* This module implements the Coercions transitive closure *)
 
+val set_close_coercion_graph : 
+  (RefinementTool.kit -> 
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  string (* baseuri *) ->
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
+  -> unit
+
 val close_coercion_graph:
   RefinementTool.kit -> 
   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
index 07d7fc08b60772bc58d7238de7f06b5e14dcff3f..b52cdc6b3b99776b086fd07a406966bf3b87df3e 100644 (file)
@@ -17,6 +17,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \
 paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
     paramodulation/indexing.cmi paramodulation/equality.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
+compose.cmi: proofEngineTypes.cmi 
 introductionTactics.cmi: proofEngineTypes.cmi 
 eliminationTactics.cmi: proofEngineTypes.cmi 
 negationTactics.cmi: proofEngineTypes.cmi 
@@ -30,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
 declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
@@ -61,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
+closeCoercionGraph.cmo: closeCoercionGraph.cmi 
+closeCoercionGraph.cmx: closeCoercionGraph.cmi 
 universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi 
 universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi 
 autoTypes.cmo: autoTypes.cmi 
@@ -107,6 +111,10 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
 variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
     proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     variousTactics.cmi 
+compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
+    closeCoercionGraph.cmi compose.cmi 
+compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
+    closeCoercionGraph.cmx compose.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -196,13 +204,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
     primitiveTactics.cmi negationTactics.cmi inversion.cmi \
     introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
     equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
-    auto.cmi tactics.cmi 
+    compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi 
 tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
     ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
     primitiveTactics.cmx negationTactics.cmx inversion.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
-    auto.cmx tactics.cmi 
+    compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi 
 declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
index 07d7fc08b60772bc58d7238de7f06b5e14dcff3f..b52cdc6b3b99776b086fd07a406966bf3b87df3e 100644 (file)
@@ -17,6 +17,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \
 paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
     paramodulation/indexing.cmi paramodulation/equality.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
+compose.cmi: proofEngineTypes.cmi 
 introductionTactics.cmi: proofEngineTypes.cmi 
 eliminationTactics.cmi: proofEngineTypes.cmi 
 negationTactics.cmi: proofEngineTypes.cmi 
@@ -30,6 +31,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
 declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
@@ -61,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
+closeCoercionGraph.cmo: closeCoercionGraph.cmi 
+closeCoercionGraph.cmx: closeCoercionGraph.cmi 
 universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi 
 universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi 
 autoTypes.cmo: autoTypes.cmi 
@@ -107,6 +111,10 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
 variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
     proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     variousTactics.cmi 
+compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
+    closeCoercionGraph.cmi compose.cmi 
+compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
+    closeCoercionGraph.cmx compose.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -196,13 +204,13 @@ tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
     primitiveTactics.cmi negationTactics.cmi inversion.cmi \
     introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
     equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
-    auto.cmi tactics.cmi 
+    compose.cmi closeCoercionGraph.cmi auto.cmi tactics.cmi 
 tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
     ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
     primitiveTactics.cmx negationTactics.cmx inversion.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
-    auto.cmx tactics.cmi 
+    compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi 
 declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
index e6f63eac0a5ee0e9e28018d161f1a1b5efc84c38..b576f830b5f94909acd7e9f893b8eeff74a2d1fd 100644 (file)
@@ -10,6 +10,7 @@ INTERFACE_FILES = \
        autoTypes.mli \
        autoCache.mli \
        paramodulation/utils.mli \
+       closeCoercionGraph.mli \
        paramodulation/subst.mli \
        paramodulation/equality.mli\
        paramodulation/founif.mli\
@@ -17,6 +18,7 @@ INTERFACE_FILES = \
        paramodulation/indexing.mli \
        paramodulation/saturation.mli \
        variousTactics.mli \
+       compose.mli \
        introductionTactics.mli eliminationTactics.mli negationTactics.mli \
        equalityTactics.mli \
        auto.mli \
diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
new file mode 100644 (file)
index 0000000..a009944
--- /dev/null
@@ -0,0 +1,371 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *)
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+(* given the new coercion uri from src to tgt returns the list 
+ * of new coercions to create. hte list elements are
+ * (source, list of coercions to follow, target)
+ *)
+let get_closure_coercions src tgt uri coercions =
+  let eq_carr s t = 
+    try
+      CoercDb.eq_carr s t
+    with
+    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+  in
+  match src,tgt with
+  | CoercDb.Uri _, CoercDb.Uri _ ->
+      let c_from_tgt = 
+        List.filter 
+          (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) 
+          coercions 
+      in
+      let c_to_src = 
+        List.filter 
+          (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) 
+          coercions 
+      in
+        (HExtlib.flatten_map 
+          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+        (HExtlib.flatten_map 
+          (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+        (HExtlib.flatten_map 
+          (fun (s,_,u1l) ->
+            HExtlib.flatten_map 
+              (fun (_,t,u2l) ->
+                HExtlib.flatten_map
+                  (fun u1 ->
+                    List.map 
+                      (fun u2 -> (s,[u1;uri;u2],t)) 
+                      u2l)
+                  u1l) 
+              c_from_tgt) 
+          c_to_src)
+  | _ -> [] (* do not close in case source or target is not an indty ?? *)
+;;
+
+let obj_attrs n = [`Class (`Coercion n); `Generated]
+
+exception UnableToCompose
+
+(* generate_composite (c2 (c1 s)) in the universe graph univ
+ * 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 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
+    | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
+  in
+  let rec mk_lambda_spline c namer = function
+    | 0 -> c
+    | n -> 
+        Cic.Lambda 
+          (namer n,
+           (Cic.Implicit None), 
+           mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1))
+  in 
+  let count_saturations_needed t arity = 
+    let rec aux acc n = function
+      | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> 
+          aux (acc@[name]) (n+1) t
+      | _ -> n,acc
+    in
+    let len,names = aux [] 0 t in
+    let len = len - arity in
+    List.fold_left 
+      (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) 
+      names
+  in
+  let compose c1 nc1 c2 nc2 =
+    Cic.Lambda 
+      (Cic.Name "x", (Cic.Implicit None),
+          (Cic.Appl (  CicSubstitution.lift 1 c2 :: mk_implicits nc2 @ 
+            [ Cic.Appl (  CicSubstitution.lift 1 c1 :: mk_implicits nc1 @ 
+             [if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
+            ])))
+  in
+(*
+  let order_metasenv metasenv = 
+    let module OT = struct type t = int let compare = Pervasives.compare end in
+    let module S = HTopoSort.Make (OT) in
+    let dep i = 
+      let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+      let metas = List.map fst (CicUtil.metas_of_term ty) in
+      HExtlib.list_uniq (List.sort Pervasives.compare metas)
+    in
+    let om =  
+      S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep 
+    in
+    List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
+  in 
+*)
+  let rec create_subst_from_metas_to_rels n = function 
+    | [] -> []
+    | (metano, ctx, ty)::tl -> 
+        (metano,(ctx,Cic.Rel (n+1),ty)) ::
+          create_subst_from_metas_to_rels (n-1) tl
+  in
+  let split_metasenv metasenv n =
+    List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
+  in
+  let purge_unused_lambdas metasenv t =
+    let rec aux = function
+        | Cic.Lambda (_, Cic.Meta (i,_), t) when  
+          List.exists (fun (j,_,_) -> j = i) metasenv ->
+            aux (CicSubstitution.subst (Cic.Rel ~-100) t)
+        | Cic.Lambda (name, s, t) -> 
+            Cic.Lambda (name, s, aux t)
+        | t -> t
+    in
+    aux t
+  in
+  let order_body_menv term body_metasenv =
+    let rec purge_lambdas = function
+      | Cic.Lambda (_,_,t) -> purge_lambdas t
+      | t -> t
+    in
+    let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+    let metas_that_saturate l =
+      List.fold_left 
+        (fun (acc,n) t ->
+          let metas = CicUtil.metas_of_term t in
+          let metas = List.map fst metas in
+          let metas = 
+            List.filter 
+              (fun i -> List.for_all (fun (j,_) -> j<>i) acc) 
+              metas 
+          in
+          let metas = List.map (fun i -> i,n) metas in
+          metas @ acc, n+1)
+        ([],0) l
+    in
+    let l_c2 = skip_appl (purge_lambdas term) in
+    let l_c1 = 
+      match HExtlib.list_last l_c2 with
+      | Cic.Appl l -> List.tl l
+      | _ -> assert false
+    in
+    (* i should cut off the laet elem of l_c2 *)
+    let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
+    List.sort 
+      (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
+          try List.assoc i meta2no -  List.assoc j meta2no 
+          with Not_found -> 
+            assert false) 
+      body_metasenv
+  in
+  let namer l n = 
+    let l = List.map (function Cic.Name s -> s | _ -> "A") l in
+    let l = List.fold_left
+      (fun acc s -> 
+        let rec add' s =
+          if List.exists ((=) s) acc then add' (s^"'") else s
+        in
+        acc@[add' s])
+      [] l
+    in
+    let l = List.rev l in 
+    Cic.Name (List.nth l (n-1))
+  in 
+  debug_print (lazy ("\nCOMPOSING"));
+  debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
+  debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
+  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
+  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
+  let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
+  let spline_len = saturations_for_c1 + saturations_for_c2 in
+  let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
+  debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
+  let c, metasenv, univ = 
+    try
+      let term, ty, metasenv, ugraph = 
+        CicRefine.type_of_aux' metasenv context c univ
+      in
+      debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+(*       let metasenv = order_metasenv metasenv in *)
+(*       debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *)
+      let body_metasenv, lambdas_metasenv = 
+        split_metasenv metasenv (spline_len + List.length context)
+      in
+      debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
+      debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
+      let body_metasenv = order_body_menv term body_metasenv in
+      debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
+      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
+      debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
+      let term, ty, metasenv, ugraph = 
+        CicRefine.type_of_aux' metasenv context term ugraph
+      in
+      let body_metasenv, lambdas_metasenv = 
+        split_metasenv metasenv (spline_len + List.length context)
+      in
+      let term = purge_unused_lambdas lambdas_metasenv term in
+      debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
+      debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+      term, metasenv, ugraph
+    with
+    | CicRefine.RefineFailure s 
+    | CicRefine.Uncertain s -> debug_print s; 
+        raise UnableToCompose
+  in  
+  c, metasenv, univ 
+;;
+
+let build_obj c univ arity =
+  let c_ty,univ = 
+    try 
+      CicTypeChecker.type_of_aux' [] [] c univ
+    with CicTypeChecker.TypeCheckerFailure s ->
+      debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) (Lazy.force s)));
+      raise UnableToCompose
+  in
+  let cleaned_ty =
+    FreshNamesGenerator.clean_dummy_dependent_types c_ty 
+  in
+  let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in 
+    obj,univ
+;;
+
+(* removes from l the coercions that are in !coercions *)
+let filter_duplicates l coercions =
+  List.filter (
+      fun (src,l1,tgt) ->
+        not (List.exists (fun (s,t,l2) -> 
+          CoercDb.eq_carr s src && 
+          CoercDb.eq_carr t tgt &&
+          try 
+            List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+          with
+          | Invalid_argument "List.for_all2" -> false)
+        coercions))
+  l
+
+let mangle s t l = 
+  (*List.fold_left
+    (fun s x -> s ^ "_" ^ x)
+    (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*)
+  s ^ "_OF_" ^ t
+;;
+
+exception ManglingFailed of string 
+
+let number_if_already_defined buri name l =
+  let err () =
+    raise 
+      (ManglingFailed 
+        ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
+  in
+  let rec aux n =
+    let suffix = if n > 0 then string_of_int n else "" in
+    let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
+    let uri = UriManager.uri_of_string suri in
+    let retry () = 
+      if n < 100 then 
+        begin
+          HLog.warn ("Uri " ^ suri ^ " already exists.");
+          aux (n+1)
+        end
+      else
+        err ()
+    in
+    if List.exists (UriManager.eq uri) l then retry ()
+    else
+      try
+        let _  = Http_getter.resolve' ~writable:true uri in
+        if Http_getter.exists' uri then retry () else uri
+      with 
+      | Http_getter_types.Key_not_found _ -> uri
+      | Http_getter_types.Unresolvable_URI _ -> assert false
+  in
+  aux 0
+;;
+  
+(* given a new coercion uri from src to tgt returns 
+ * a list of (new coercion uri, coercion obj, universe graph) 
+ *)
+let close_coercion_graph _ src tgt uri baseuri =
+  (* check if the coercion already exists *)
+  let coercions = CoercDb.to_list () in
+  let todo_list = get_closure_coercions src tgt uri coercions in
+  let todo_list = filter_duplicates todo_list coercions in
+  try
+    let new_coercions = 
+      List.fold_left 
+        (fun acc (src, l , tgt) ->
+          try 
+            (match l with
+            | [] -> assert false 
+            | he :: tl ->
+                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+                let first_step = 
+                  Cic.Constant ("", 
+                    Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                    Cic.Sort Cic.Prop, [], obj_attrs arity)
+                in
+                let o,_ = 
+                  List.fold_left (fun (o,univ) coer ->
+                    match o with 
+                    | Cic.Constant (_,Some c,_,[],_) ->
+                        let t, menv, univ = 
+                          generate_composite c 
+                            (CoercDb.term_of_carr (CoercDb.Uri coer)) 
+                            [] [] univ arity true
+                        in
+                        assert (menv = []);
+                        build_obj t univ arity
+                    | _ -> assert false 
+                  ) (first_step, CicUniv.empty_ugraph) tl
+                in
+                let name_src = CoercDb.name_of_carr src in
+                let name_tgt = CoercDb.name_of_carr tgt in
+                let by = List.map UriManager.name_of_uri l in
+                let name = mangle name_tgt name_src by in
+                let c_uri = 
+                  number_if_already_defined baseuri name 
+                    (List.map (fun (_,_,u,_) -> u) acc) 
+                in
+                let named_obj = 
+                  match o with
+                  | Cic.Constant (_,bo,ty,vl,attrs) ->
+                      Cic.Constant (name,bo,ty,vl,attrs)
+                  | _ -> assert false 
+                in
+                  (src,tgt,c_uri,named_obj))::acc
+          with UnableToCompose -> acc
+      ) [] todo_list
+    in
+    new_coercions
+  with ManglingFailed s -> HLog.error s; []
+;;
+
+CicCoercion.set_close_coercion_graph close_coercion_graph;;
diff --git a/components/tactics/closeCoercionGraph.mli b/components/tactics/closeCoercionGraph.mli
new file mode 100644 (file)
index 0000000..d0bdb44
--- /dev/null
@@ -0,0 +1,40 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* This module implements the Coercions transitive closure *)
+
+val close_coercion_graph:
+  RefinementTool.kit -> 
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  string (* baseuri *) ->
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+
+exception UnableToCompose
+
+val generate_composite:
+  Cic.term -> Cic.term -> Cic.context -> 
+  Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> 
+    bool (* last lambda goes with innermost arg *) ->
+    Cic.term * Cic.metasenv * CicUniv.universe_graph
diff --git a/components/tactics/compose.ml b/components/tactics/compose.ml
new file mode 100644 (file)
index 0000000..f090c3d
--- /dev/null
@@ -0,0 +1,73 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 (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
+      try
+        let t, menv, _ =
+          CloseCoercionGraph.generate_composite t1 t2 context menv
+            CicUniv.oblivion_ugraph arity false
+        in
+        generate (arity - 1) menv (t::acc)
+      with 
+      | CloseCoercionGraph.UnableToCompose -> generate (arity - 1) menv acc
+  in
+  let terms, metasenv = generate (count_pi ty1) metasenv [] in
+  let proof = 
+    let uri, _, _subst, bo, ty, attrs = proof in
+    uri, metasenv, _subst, bo, ty, attrs
+  in
+  let proof, goal =
+    List.fold_left 
+      (fun (proof,goal) t ->
+        let lazy_of t =
+          ProofEngineTypes.const_lazy_term t
+        in
+        let proof, gl = 
+          ProofEngineTypes.apply_tactic
+            (VariousTactics.generalize_tac (Some (lazy_of t), [], None))
+            (proof,goal)
+        in
+        assert(List.length gl = 1);
+        proof,List.hd gl)
+      (proof,goal) terms
+  in
+  ProofEngineTypes.apply_tactic 
+    (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
+    (proof,goal)
+;;
+
+let compose_tac ?howmany ?mk_fresh_name_callback t1 t2 =
+  ProofEngineTypes.mk_tactic 
+    (compose_tac ?howmany ?mk_fresh_name_callback t1 t2)
+;;
diff --git a/components/tactics/compose.mli b/components/tactics/compose.mli
new file mode 100644 (file)
index 0000000..37e69d4
--- /dev/null
@@ -0,0 +1,29 @@
+(* Copyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+val compose_tac: 
+  ?howmany:int -> 
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  Cic.term -> Cic.term -> ProofEngineTypes.tactic
index 527a8abb3bbb4b531a32bf95344ee767432ec2d1..1ccd2adcb0ab0d655438ca858d56770ceec76e0b 100644 (file)
@@ -71,3 +71,7 @@ let symmetry = EqualityTactics.symmetry_tac
 let transitivity = EqualityTactics.transitivity_tac
 let unfold = ReductionTactics.unfold_tac
 let whd = ReductionTactics.whd_tac
+let compose = Compose.compose_tac
+
+(* keep linked *)
+let _ = CloseCoercionGraph.close_coercion_graph;;
index 70773a4a7fd41bf370ffe9ddde6d4a94a91de865..4307e6b034f4f82729ecda83cccd93e8c4e23a90 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri May 25 11:09:42 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun  1 13:27:04 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -102,3 +102,7 @@ val unfold :
   Cic.lazy_term option ->
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 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
index 36a1f0b29e22e3fa14a24c086a432d5241b97b47..fbf7f2ab2edc94f92d34405033f677d0a83dba97 100644 (file)
     <keyword>absurd</keyword>
     <keyword>apply</keyword>
     <keyword>assumption</keyword>
-    <keyword>auto</keyword>
-    <keyword>paramodulation</keyword>
+    <keyword>autobatch</keyword>
     <keyword>cases</keyword>
     <keyword>clear</keyword>
     <keyword>clearbody</keyword>
     <keyword>change</keyword>
+    <keyword>compose</keyword>
     <keyword>constructor</keyword>
     <keyword>contradiction</keyword>
     <keyword>cut</keyword>
     <keyword>check</keyword>
     <keyword>hint</keyword>
     <keyword>set</keyword>
+    <keyword>auto</keyword>
   </keyword-list>
   
   <keyword-list _name = "Whelp Macro" style = "Others 3"