]> matita.cs.unibo.it Git - helm.git/commitdiff
new universes implementation
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Jun 2004 13:44:34 +0000 (13:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 1 Jun 2004 13:44:34 +0000 (13:44 +0000)
31 files changed:
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/testlibrary.ml
helm/ocaml/cic/cicUniv.ml
helm/ocaml/cic/cicUniv.mli
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_proof_checking/cicEnvironment.ml
helm/ocaml/cic_proof_checking/cicEnvironment.mli
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.mli
helm/ocaml/cic_unification/cicRefine.ml
helm/ocaml/getter/.depend
helm/ocaml/tactics/.depend
helm/ocaml/tactics/Makefile
helm/ocaml/tactics/discriminationTactics.ml
helm/ocaml/tactics/eliminationTactics.ml
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/fourierR.ml
helm/ocaml/tactics/introductionTactics.ml
helm/ocaml/tactics/negationTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineStructuralRules.ml
helm/ocaml/tactics/proofEngineTypes.ml
helm/ocaml/tactics/proofEngineTypes.mli [new file with mode: 0644]
helm/ocaml/tactics/reductionTactics.ml
helm/ocaml/tactics/ring.ml
helm/ocaml/tactics/statefulProofEngine.ml
helm/ocaml/tactics/tacticChaser.ml
helm/ocaml/tactics/tacticals.ml
helm/ocaml/tactics/variousTactics.ml
helm/ocaml/tactics/variousTactics.mli

index bda4c4b826126a2caf354bfdd5e7838227e6f8d6..eeb6053aa2615b86a75efc5723d7193894896f3b 100644 (file)
@@ -469,6 +469,11 @@ let qed () =
     None -> assert false
   | Some (uri,[],bo,ty) ->
      let uri = match uri with Some uri -> uri | _ -> assert false in
+     (* we want to typecheck in the ENV *)
+     (*let old_working = CicUniv.get_working () in
+     CicUniv.set_working (CicUniv.get_global ());*)
+     CicUniv.directly_to_env_begin () ;
+     prerr_endline "-------------> QED";
      if
       CicReduction.are_convertible []
        (CicTypeChecker.type_of_aux' [] [] bo) ty
@@ -484,7 +489,16 @@ let qed () =
         let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
          make_dirs pathname ;
          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
-          pathname
+          pathname;
+       (* add the object to the env *)
+       CicEnvironment.add_type_checked_term uri (
+        Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+       (* FIXME: the variable list!! *)
+       (*
+       CicUniv.qed (); (* now the env has the right constraints *)*)
+       CicUniv.directly_to_env_end();
+       CicUniv.reset_working ();
+     prerr_endline "-------------> FINE";
       end
      else
       raise WrongProof
@@ -1593,7 +1607,8 @@ let open_ () =
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
-     CicTypeChecker.typecheck uri ;
+     ignore(CicTypeChecker.typecheck uri);
+     (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
      let metasenv,bo,ty =
       match CicEnvironment.get_cooked_obj uri with
          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
index d9b6219b2d159032f13af762923a069794f7e6c8..ab8d4327a2b5dde24ba74120519177e1d3b6a5db 100644 (file)
@@ -58,11 +58,12 @@ let get_current_status_as_xml () =
 ;;
 
 let apply_tactic ~tactic =
+ let module PET = ProofEngineTypes in
  match get_proof (),!goal with
   | None,_
   | _,None -> assert false
   | Some proof', Some goal' ->
-     let (newproof, newgoals) = tactic (proof', goal') in
+     let (newproof, newgoals) = PET.apply_tactic tactic (proof', goal') in
       set_proof (Some newproof);
       goal :=
        (match newgoals, newproof with
index ee1b982c41547aa6526628997d646226e316f52f..fccdc19c619530b67093437c77a00254b2534869 100644 (file)
@@ -112,10 +112,12 @@ let test_uri uri =
      (* We do this to clear the alarm set by the signal handler *)
      ignore (Unix.alarm 0) ;
      `TimeOut
+     (*
   | exn ->
       prerr_endline (sprintf "Top Level Uncaught Exception: %s"
         (Printexc.to_string exn));
-      `Nok
+      `Nok*)
+  | exn -> raise exn
 
 let report (ok,nok,maybe,timeout) =
   print_newline ();
index d76fde47a535c3582f26e81e26ef57e0c0a96ca1..05e0a99a1e9f7435902328ce7f988d06894f1cdc 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-(* 
+open Printf
 
-   todo:
-     - in add_eq there is probably no need of add_gt, simple @ the gt lists 
-     - the problem of duplicates in the 1steg gt/ge list if two of them are
-       add_eq may be "fixed" in some ways:
-        - lazy, do nothing on add_eq and eventually update the ge list 
-         on closure
-       - add a check_duplicates_after_eq function called by add_eq
-       - do something like rmap, add a list of canonical that point to us
-         so when we collapse we have the list of the canonical we may update
-     - don't use failure but another exception
-     
-*)
+(******************************************************************************)
+(** Types and default values                                                 **)
+(******************************************************************************)
 
-(* ************************************************************************** *)
-(*  TYPES                                                                     *)
-(* ************************************************************************** *)
-type universe = int 
-
-type canonical_repr = {
-        mutable ge:universe list; 
-        mutable gt:universe list;
-       (* since we collapse we may need the reverse map *) 
-        mutable eq:universe list; 
-       (* the canonical representer *)
-        u:universe
-}
+type universe = int
 
 module UniverseType = struct
   type t = universe
   let compare = Pervasives.compare
 end
 
-module MapUC = Map.Make(UniverseType)
+module SOF = Set.Make(UniverseType)
 
-(* ************************************************************************** *)
-(*  Globals                                                                   *)
-(* ************************************************************************** *)
+type entry = {
+       eq_closure : SOF.t;
+       ge_closure : SOF.t;
+       gt_closure : SOF.t;
+       in_eq_of   : SOF.t;
+       in_ge_of   : SOF.t;
+       in_gt_of   : SOF.t;
+       one_s_eq   : SOF.t;
+       one_s_ge   : SOF.t;
+       one_s_gt   : SOF.t;
+}
 
-let map = ref MapUC.empty 
-let used = ref (-1)
+module MAL = Map.Make(UniverseType)
 
-(* ************************************************************************** *)
-(*  Helpers                                                                   *)
-(* ************************************************************************** *)
+type arc_type = GE | GT | EQ
 
-(* create a canonical for [u] *)
-let mk_canonical u =
-  {u = u ; gt = [] ; ge = [] ; eq = [u] }
+type arc = arc_type * universe * universe
 
-(* give a new universe *)
-let fresh () = 
-  used := !used + 1;
-  map := MapUC.add !used (mk_canonical !used) !map;
-  !used
-  
-let reset () =
-  map := MapUC.empty;
-  used := -1
+type bag = entry MAL.t * (arc list)
+
+let empty_entry = {
+       eq_closure=SOF.empty;
+       ge_closure=SOF.empty;
+       gt_closure=SOF.empty;
+       in_eq_of=SOF.empty;
+       in_ge_of=SOF.empty;
+       in_gt_of=SOF.empty;
+       one_s_eq=SOF.empty;
+       one_s_ge=SOF.empty;
+       one_s_gt=SOF.empty;
+}
+
+let empty_bag = (MAL.empty, [])
+
+let env_bag = ref empty_bag
+
+(******************************************************************************)
+(** Pretty printings                                                         **)
+(******************************************************************************)
+
+let string_of_universe u = string_of_int u
+
+let string_of_arc_type u =
+  match u with
+    EQ -> "EQ" 
+  | GT -> "GT"
+  | GE -> "EQ"
+
+let string_of_arc u = 
+  let atype,a,b = u in
+  (string_of_arc_type atype) ^ " " ^ 
+   (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; "
+;;
+
+let string_of_universe_set l = 
+  SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
+
+let string_of_arc_list l = 
+  List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l
+
+let string_of_node n =
+  "{"^
+  "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ 
+  "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ 
+  "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ 
+  "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^ 
+  "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^ 
+  "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n"
   
-(* ************************************************************************** *)
-(*   Pretty printing                                                          *)
-(* ************************************************************************** *) 
-(* pp *)
-let string_of_universe = string_of_int
-
-(* pp *)
-let canonical_to_string c = 
-  let s_gt = 
-    List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in
-  let s_ge = 
-    List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in  
-  let s_eq =
-    List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in
-  let s_u = (string_of_universe c.u) in
-  "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}"
-
-(* print the content of map *)
-let print_map () =
-  MapUC.iter (fun u c -> 
-   prerr_endline 
-    (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c))) 
-  !map;
-  prerr_endline ""
-
-(* ************************************************************************** *)
-(*  The way we fail                                                           *)
-(* ************************************************************************** *)   
-(* we are doing bad *)
-let error s = 
-  (*prerr_endline " ======= Universe Inconsistency =========";
-  print_map ();*)
-  prerr_endline (" " ^ s ^ "\n");
-  failwith s
-
-(* ************************************************************************** *)
-(*  The real code                                                             *)
-(* ************************************************************************** *) 
-(* <--------> *)
-
-(* the canonical representer of the [u] equaliti class *)
-let repr u = 
+let string_of_mal m =
+  let rc = ref "" in
+  MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m;
+  !rc
+
+let string_of_bag b = 
+  let (m,l) = b in
+  let s_m = string_of_mal m in
+  let s_l = string_of_arc_list l in
+   s_m ^"["^s_l^"]"
+
+(******************************************************************************)
+(** Helpers                                                                  **)
+(******************************************************************************)
+
+(*
+    we need to merge the 2 graphs... here the code 
+*)
+let repr u m =
   try 
-    MapUC.find u !map
+    MAL.find u m
   with
-    Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u))
-
-(* all the nodes we can ifer in the ge list of u *)
-let close_ge u =
-  let repr_u = repr u in
-  let rec close_ge_aux tofollow bag = 
-    match tofollow with
-      [] -> bag
-    | v::tl -> let repr_v = repr v in
-               if List.mem repr_v bag then (* avoid loops *)
-                 (close_ge_aux tl bag ) 
-               else
-                 (close_ge_aux (tl @ repr_v.ge) (repr_v::bag))
-                 (* we assume that v==u -> v \notin (repr u).ge *)
-  in
-  close_ge_aux repr_u.ge []
+    Not_found -> 
+      try 
+        let m',_ = !env_bag in
+        MAL.find u m'
+      with
+        Not_found -> empty_entry
+    
+(*
+    FIXME: May be faster if we make it by hand
+*)
+let merge_closures f nodes m =  
+  SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
 
-(* all the nodes we can ifer in the gt list of u,
-   we must follow bot gt and ge arcs, but we must put in bag only 
-   the nodes that have a gt in theys path 
+(******************************************************************************)
+(** Real stuff GT                                                            **)
+(******************************************************************************)
+
+(* 
+    todo is the SOF of nodes that needs to be recomputed, 
+    m is the MAL map, s is the already touched nodes 
 *)
-let close_gt u =
-  let repr_u = repr u in
-  let rec close_gt_aux bag todo inspected =
-    (*print_all bag todo;Unix.sleep 1;*)
-    match todo with
-      [],[] -> bag
-    | [],p::may -> let repr_p = repr p in 
-                   if List.mem repr_p.u inspected then (* avoid loops *)
-                     close_gt_aux bag ([],may) inspected
-                   else 
-                     close_gt_aux bag (repr_p.gt,repr_p.ge @ may) 
-                      (repr_p.u::inspected)
-    | s::secure,may -> let repr_s = repr s in
-                       if List.mem repr_s.u inspected then (* avoid loops *)
-                         if List.mem repr_s bag then
-                           close_gt_aux bag (secure,may) inspected
-                         else
-                           (* even if we ave already inspected the node, now
-                              it is in the secure list so we want it in the bag 
-                           *)
-                           close_gt_aux (repr_s::bag) (secure,may) inspected
-                       else
-                         close_gt_aux ((repr_s)::bag) 
-                          (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected)
-  in
-  close_gt_aux [] (repr_u.gt,repr_u.ge) []
-  
-(* when we add an eq we have to change the mapping of u to c*)
-let remap u c =
-  let repr_u = repr u in
-  List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq;
-  List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq
-
-(* we suspect that u and v are connected by a == implyed by two >= *)
-let rec collapse u v = 
-  let repr_u = repr u in
-  let repr_v = repr v in
-  let ge_v = close_ge v in
-  let ge_u = close_ge u in
-  if List.mem repr_u ge_v && List.mem repr_v ge_u then
-    add_eq u v
-
-(* we have to add u == v *)
-and add_eq u v = 
-  let repr_u = repr u in
-  let repr_v = repr v in
-  (* if we already have u == v then do nothing *)
-  if repr_u = repr_v then
-    () 
+let rec redo_gt_closure todo m s =
+  if SOF.is_empty todo then m
   else
-    (* if we already have v > u then fail *)
-    let gt_v = close_gt v in
-    if List.mem repr_u gt_v then
-      error ("Asking for " ^ (string_of_universe u) ^ " == " ^ 
-            (string_of_universe v) ^ " but " ^ 
-            (string_of_universe v) ^ " > " ^ (string_of_universe u))
-    else 
-      (* if we already have u > v then fail *)
-      let gt_u = close_gt u in
-      if List.mem repr_v gt_u then           
-        error ("Asking for " ^ (string_of_universe u) ^ " == " ^ 
-              (string_of_universe v) ^ " but " ^ 
-              (string_of_universe u) ^ " > " ^ (string_of_universe v))
-      else
-        (* add the inherited > constraints *)
-        List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt;
-        (* add the inherited >= constraints *)
-        (* close_ge assumes that v==u -> v \notin (repr u).ge *)
-        repr_u.ge <- List.filter (fun x -> x <> u && x <> v) 
-         (repr_v.ge @ repr_u.ge);
-        (* mege the eq list, we assume they are disjuncted *)
-        repr_u.eq <- repr_u.eq @ repr_v.eq;
-        (* we have to remap all node represented by repr_v to repr_u *)
-        remap v repr_u;
-        (* FIXME: not sure this is what we have to do 
-                  think more to the list of suspected cicles
-        *)
-        List.iter (fun x -> collapse u x) repr_u.ge 
-    
-(* we have to add u >= v *)
-and add_ge u v =
-  let repr_u = repr u in
-  let repr_v = repr v in
-  (* if we already have u == v then do nothing *)
-  if repr_u = repr_v then
-    () 
-  else 
-    (* if we already have v > u then fail *)
-    let gt = close_gt v in
-    if List.memq repr_u gt then
-      error ("Asking for " ^ (string_of_universe u) ^ " >= " ^ 
-            (string_of_universe v) ^ " but " ^ 
-            (string_of_universe v) ^ " > " ^ (string_of_universe u))
+    begin
+    (* we choose the node to recompute *)
+    let u = SOF.choose todo in
+    if not (SOF.mem u s) then
+      let ru = repr u m in
+      let ru' = {ru with gt_closure = 
+       (* the new gt closure is the gt-closures + ge-closures + eq-closures 
+          of the one step gt-connected nodes *)
+       SOF.union ru.one_s_gt (merge_closures 
+        (fun x -> SOF.union x.eq_closure 
+        (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in
+      let m' = MAL.add u ru' m in
+      let s' = SOF.add u s in
+      redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s'
     else
-      (* it is now safe to add u >= v *)
-      repr_u.ge <- v::repr_u.ge;
-      (* but we may have introduced a cicle *)
-      collapse u v (* FIXME: not sure it is from u to v, think more. *)
-      
-(* we have to add u > v *)        
-and add_gt u v =
-  let repr_u = repr u in
-  let repr_v = repr v in
-  (* if we already have u == v then fail *)
-  if repr_u = repr_v then
-    error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
-          (string_of_universe v) ^ " but " ^ 
-          (string_of_universe u) ^ " == " ^ (string_of_universe v))
-  else 
-    (* if we already have u > v do nothing *)
-    let gt_u = close_gt u in
-    if List.memq repr_v gt_u then
-      () 
+      (* if already done go next. FIXME: think if it is right
+         maybe we should check if we changed something or not *)
+      redo_gt_closure (SOF.remove u todo) m s
+    end
+
+(*
+    calculates the closures of u and adjusts the in_*_of of v, then
+    starts redo_*_closure to adjust the colure of nodew thet have 
+    (clusure u) in theyr closures
+*)
+let add_gt_arc u v m =
+  let ru = repr u m in
+  let rv = repr v m in 
+  let ru' = {
+    (* new node: we add the v gt-closure and v to our gt-closure *)
+    eq_closure = ru.eq_closure;
+    ge_closure = ru.ge_closure;
+    gt_closure = SOF.add v 
+     (SOF.union ru.gt_closure 
+      (SOF.union rv.ge_closure 
+       (SOF.union rv.eq_closure rv.gt_closure)));
+    in_eq_of = ru.in_eq_of;
+    in_ge_of = ru.in_ge_of;
+    in_gt_of = ru.in_gt_of;
+    one_s_eq = ru.one_s_eq;
+    one_s_ge = ru.one_s_ge;
+    one_s_gt = SOF.add v ru.one_s_gt;
+  } in
+  (* may add the sanity check *)
+  let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in
+  let m' = MAL.add u ru' m in
+  let m'' = MAL.add v rv' m' in
+  redo_gt_closure ru'.in_gt_of m'' SOF.empty
+
+(*                                                                            
+    given the 2 nodes plus the current bag, adds the arc, recomputes the 
+    closures and returns the new map
+*)                                                                            
+let add_gt u v b =
+  let m,l = b in
+  let m' = add_gt_arc u v m in
+  let l' = (GT,u,v)::l in
+  (m',l')
+
+(******************************************************************************)
+(** Real stuff GE                                                            **)
+(******************************************************************************)
+
+(* 
+    todo is the SOF of nodes that needs to be recomputed, 
+    m is the MAL map, s is the already touched nodes 
+*)
+let rec redo_ge_closure todo m s =
+  if SOF.is_empty todo then m,s
+  else
+    begin
+    let u = SOF.choose todo in
+    if not (SOF.mem u s) then
+      begin
+        let ru = repr u m in
+       (* the ge-closure is recomputed as the ge-closures of  
+          ge connected nodes plus theys eq-closure *)
+        let ru' = {ru with ge_closure = merge_closures 
+          (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in
+        let m' = MAL.add u ru' m in
+        let s' = SOF.add u s in
+        redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s'
+      end
     else
-      (* if we already have v > u then fail *)
-      let gt = close_gt v in
-      if List.memq repr_u gt then
-        error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
-              (string_of_universe v) ^ " but " ^ 
-              (string_of_universe v) ^ " > " ^ (string_of_universe u))
+      redo_ge_closure (SOF.remove u todo) m s
+    end
+
+(*
+    calculates the closures of u and adjusts the in_*_of of v, then
+    starts redo_*_closure to adjust the colure of nodew thet have 
+    (clusure u) in theyr closures
+*)
+let add_ge_arc u v m =
+  let ru = repr u m in
+   let rv = repr v m in 
+  let ru' = {
+    eq_closure = ru.eq_closure;
+    ge_closure = SOF.add v 
+     (SOF.union ru.ge_closure 
+      (SOF.union rv.eq_closure rv.ge_closure));
+    gt_closure = ru.gt_closure;
+    in_eq_of = ru.in_eq_of;
+    in_ge_of = ru.in_ge_of;
+    in_gt_of = ru.in_gt_of;
+    one_s_eq = ru.one_s_eq;
+    one_s_ge = SOF.add v ru.one_s_ge;
+    one_s_gt = ru.one_s_gt;
+  } in
+  let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in
+  let m' = MAL.add u ru' m in
+  let m'' = MAL.add v rv' m' in
+  let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
+  (* closing ge may provoke aome changes in gt-closures *)
+  redo_gt_closure (SOF.union ru'.in_gt_of 
+   (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of)) 
+    td SOF.empty )) m''' SOF.empty
+
+(*                                                                            
+    given the 2 nodes plus the current bag, adds the arc, recomputes the 
+    closures and returns the new map
+*) 
+let add_ge u v b =
+  let m,l = b in
+  let m' = add_ge_arc u v m in
+  let l' = (GE,u,v)::l in
+  (m',l')
+  
+(******************************************************************************)
+(** Real stuff EQ                                                            **)
+(******************************************************************************)
+
+let rec redo_eq_closure todo m s =
+  if SOF.is_empty todo then m,s
+  else begin
+    let u = SOF.choose todo in
+    if not (SOF.mem  u s) then
+      begin
+        let ru = repr u m in
+        let eq_closure = merge_closures 
+          (fun x -> x.eq_closure) ru.one_s_eq m in
+        let ru' = {ru with eq_closure = eq_closure
+        ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
+        let m' = MAL.add u ru' m in
+        let s' = SOF.add u s in
+        redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
+      end
+    else
+      redo_eq_closure (SOF.remove u todo) m s
+  end
+
+(*
+    calculates the closures of u and adjusts the in_*_of of v, then
+    starts redo_*_closure to adjust the colure of nodew thet have 
+    (clusure u) in theyr closures
+*)
+let add_eq_arc u v m =
+  let ru = repr u m in
+  let rv = repr v m in 
+  (* since eq is symmetric we have to chage more *)
+  let eq_closure = SOF.add u (SOF.add v 
+     (SOF.union ru.eq_closure rv.eq_closure)) in
+  let ru' = {
+    eq_closure = eq_closure;
+    ge_closure = SOF.union ru.ge_closure rv.ge_closure;
+    gt_closure = SOF.union ru.gt_closure rv.gt_closure;
+    in_eq_of = eq_closure;
+    in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
+    in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
+    one_s_eq = eq_closure;
+    one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
+    one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
+  } in
+  (* this is a collapse *)
+  let rv' = ru' in
+  let m' = MAL.add u ru' m in
+  let m'' = MAL.add v rv' m' in
+  let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
+  (* redoing a eq may change some ge and some gt *)
+  let m'''',td' = redo_ge_closure 
+   (SOF.union ru'.in_ge_of 
+    (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of)) 
+    td SOF.empty)) m''' SOF.empty in
+  redo_gt_closure (SOF.union ru'.in_gt_of 
+   (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of)) 
+    td' SOF.empty)) m'''' SOF.empty
+
+(*                                                                            
+    given the 2 nodes plus the current bag, adds the arc, recomputes the 
+    closures and returns the new map
+*) 
+let add_eq u v b =
+  let m,l = b in
+  let m' = add_eq_arc u v m in
+  let l' = (EQ,u,v)::l in
+  (m',l')
+
+(******************************************************************************)
+(** Oyther real code                                                         **)
+(******************************************************************************)
+
+exception UniverseInconsistency of string 
+
+let error arc node1 closure_type node2 closure =
+  let s = "  ===== Universe Inconsistency detected =====\n\n" ^
+   "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^ 
+   (string_of_universe node1) ^ " is in the " ^
+   (string_of_arc_type closure_type) ^ " closure {" ^
+   (string_of_universe_set closure) ^ "} of " ^ 
+   (string_of_universe node2) ^ "\n\n" ^
+   "  ===== Universe Inconsistency detected =====\n" in
+  prerr_endline s;
+  raise (UniverseInconsistency s)
+
+(*  
+    we merge the env_bag with b
+*)
+let qed b = 
+  let m,l = b in
+  let m',l' = !env_bag in
+  let m'' = ref m' in
+  MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
+  let l'' = l @ l' in
+  env_bag := (!m'',l'')
+  
+let add_eq u v b =
+  (* should we check to no add twice the same?? *)
+  let m,_ = b in
+  let ru = repr u m in
+  if SOF.mem v ru.gt_closure then
+    error (EQ,u,v) v GT u ru.gt_closure
+  else
+    begin
+    let rv = repr v m in
+    if SOF.mem u rv.gt_closure then
+      error (EQ,u,v) u GT v rv.gt_closure
+    else
+      add_eq u v b
+    end
+
+let add_ge u v b =
+  (* should we check to no add twice the same?? *)
+  let m,_ = b in
+  let rv = repr v m in
+  if SOF.mem u rv.gt_closure then
+    error (GE,u,v) u GT v rv.gt_closure
+  else
+    add_ge u v b
+  
+let add_gt u v b =
+  (* should we check to no add twice the same?? *)
+  let m,_ = b in
+  let rv = repr v m in
+  if SOF.mem u rv.gt_closure then
+    error (GT,u,v) u GT v rv.gt_closure
+  else
+    begin
+      if SOF.mem u rv.ge_closure then
+        error (GT,u,v) u GE v rv.ge_closure
       else
-        (* if we already have v >= u then fail *)
-        let ge = close_ge v in
-        if List.memq repr_u ge then
-          error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
-                (string_of_universe v) ^ " but " ^ 
-                (string_of_universe v) ^ " >= " ^ (string_of_universe u))
-        else
-          (* it is safe to add u > v *)
-          repr_u.gt <- v::repr_u.gt
+        begin
+          if SOF.mem u rv.eq_closure then
+            error (GT,u,v) u EQ v rv.eq_closure
+         else
+           add_gt u v b
+       end
+    end
+  
+  
+
+(******************************************************************************)
+(** World interface                                                          **)
+(******************************************************************************)
+
+type universe_graph = bag
+
+let work_bag = ref empty_bag
+let current_index = ref (-1)
+
+let get_working () = !work_bag
+let get_global  () = !env_bag 
+let set_working b = work_bag := b
+
+let fresh () =
+  current_index := !current_index + 1;
+  !current_index
+
+let qed () = 
+  qed !work_bag
+
+let print_global_graph () =
+  let s = string_of_bag !env_bag in
+  prerr_endline s
+
+let print_working_graph () =
+  let s = string_of_bag !work_bag in
+  prerr_endline s
+
+type history_ticket = int
+
+let get_history_ticket b =
+  let m,l = b in
+  List.length l
+
+let redo_history t b b'=
+  let rec get_history l n =
+    if n == 0 then
+      []
+    else
+      begin
+      match l with 
+        [] -> failwith "erroer, lista piu' corta della history"
+      | h::tl -> h::(get_history tl (n - 1))
+      end
+  in
+  let rec redo_commands l b =
+    match l with
+      [] -> b
+    | (GE,u,v)::tl -> redo_commands tl (add_ge u v b)
+    | (GT,u,v)::tl -> redo_commands tl (add_gt u v b)
+    | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b)
+  in
+  let (m,l) = b in
+  let todo = List.rev (get_history l ((List.length l) - t)) in
+  try 
+    redo_commands todo b'
+  with 
+    UniverseInconsistency s -> failwith s
+  (*| _ -> failwith "Unexpected exception"*)
 
 let add_gt u v =
   try 
-    add_gt u v; true
+    work_bag := add_gt u v !work_bag; true
   with
-    exn -> false
+    UniverseInconsistency s -> false
+  (*| _ -> failwith "Unexpected exception"*)
 
-let add_ge u v =
+let add_ge u v = 
   try 
-    add_ge u v; true
+    work_bag := add_ge u v !work_bag;true
   with
-    exn -> false
+    UniverseInconsistency s -> false
+  (*| _ -> failwith "Unexpected exception"*)
 
 let add_eq u v =
   try 
-    add_eq u v; true
+    work_bag := add_eq u v !work_bag;true
   with
-    exn -> false
-
-(* <--------> *)
+    UniverseInconsistency s -> false
+  (*| _ -> failwith "Unexpected exception"*)
 
-(* ************************************************************************** *)
-(*  To make tests                                                             *)
-(* ************************************************************************** *)
+let saved_data = ref (empty_bag,0)
 
-(*
-let check_status_eq l =
-  let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in
-  let repr_u = repr (List.hd l) in
-  let rec check_status_eq_aux c =
-    match c with
-      [] -> print_endline (" Result check_status_eq["^s^"] = OK");true
-    | u::tl -> if repr u != repr_u then
-                 (print_endline (" Result check_status_eq["^s^"] = FAILED");
-                 print_endline ((string_of_universe u) ^ " != " ^ 
-                  (string_of_universe repr_u.u));
-                 print_map ();false)
-               else
-                 check_status_eq_aux tl
-  in
-  check_status_eq_aux (List.tl l)
-*)
+let directly_to_env_begin () =
+  saved_data := (!work_bag, get_history_ticket !env_bag);
+  work_bag := empty_bag
+  
+let directly_to_env_end () = 
+  qed ();
+  let (b,t) = !saved_data in
+  work_bag := redo_history t !env_bag b
+let reset_working () = work_bag := empty_bag
 
-(* ************************************************************************** *)
-(*  Fake implementation                                                       *)
-(* ************************************************************************** *)
+(******************************************************************************)
+(** Fake implementatoin                                                      **)
+(******************************************************************************)
 
-(* <--------> *
-let add_ge u v = true
-let add_gt u v = true
-let add_eq u v = true
-* <--------> *)
+let reset_working = function _ -> ()
+let directly_to_env_end = function _ -> ()
+let directly_to_env_begin = function _ -> ()
+let add_eq = fun _ _ -> true
+let add_ge = fun _ _ -> true
+let add_gt = fun _ _ -> true
+let get_working = function a -> empty_bag
+let set_working = function a -> ()
index d7eb7dc413e9bb6e460b3cd645f09dd2e07e2485..f98ea84c6ce411e6541cd9179c93332ecad25ef2 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* Cic.Type of universe *)
 type universe
+
+(* returns a fresh universe and puts it in the working graph *)
 val fresh: unit -> universe
+
+(* add eq/ge/gt constraints to the woring graph *)
 val add_eq: universe -> universe -> bool
 val add_ge: universe -> universe -> bool
 val add_gt: universe -> universe -> bool
 
-(*
-val string_of_universe: universe -> string
-val print_map: unit -> unit
-*)
+(* prints the graphs *)
+val print_global_graph: unit -> unit
+val print_working_graph: unit -> unit
+
+type universe_graph
+val get_working: unit -> universe_graph
+val set_working: universe_graph -> unit
+
+val directly_to_env_begin: unit -> unit
+val directly_to_env_end: unit -> unit
 
-val reset: unit -> unit
+val reset_working:  unit -> unit
 
-(* val check_status_eq: universe list -> bool *)
index f7cfce144d7b6daacbceaafdc16ef71cdbc4286d..637636e0b8b8146d62964eb8710cd7947f7bbc75 100644 (file)
@@ -204,48 +204,56 @@ let interpretate ~context ~env ast =
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
          in
-          (match cic with
-          | Cic.Const (uri, []) ->
-              let uris =
-                match CicEnvironment.get_obj uri with
-                | Cic.Constant (_, _, _, uris) -> uris
-                | _ -> assert false
-              in
-              Cic.Const (uri, mk_subst uris)
-          | Cic.Var (uri, []) ->
-              let uris =
-                match CicEnvironment.get_obj uri with
-                | Cic.Variable (_, _, _, uris) -> uris
-                | _ -> assert false
-              in
-              Cic.Var (uri, mk_subst uris)
-          | Cic.MutInd (uri, i, []) ->
-              let uris =
-                match CicEnvironment.get_obj uri with
-                | Cic.InductiveDefinition (_, uris, _) -> uris
-                | _ -> assert false
-              in
-              Cic.MutInd (uri, i, mk_subst uris)
-          | Cic.MutConstruct (uri, i, j, []) ->
-              let uris =
-                match CicEnvironment.get_obj uri with
-                | Cic.InductiveDefinition (_, uris, _) -> uris
-                | _ -> assert false
-              in
-              Cic.MutConstruct (uri, i, j, mk_subst uris)
-          | Cic.Meta _ | Cic.Implicit _ as t ->
+          (try
+            match cic with
+            | Cic.Const (uri, []) ->
+                let uris =
+                  (*match CicEnvironment.get_obj uri with*)
+                  match CicTypeChecker.typecheck uri with
+                  | Cic.Constant (_, _, _, uris) -> uris
+                  | _ -> assert false
+                in
+                Cic.Const (uri, mk_subst uris)
+            | Cic.Var (uri, []) ->
+                let uris =
+                  (*match CicEnvironment.get_obj uri with*)
+                  match CicTypeChecker.typecheck uri with
+                  | Cic.Variable (_, _, _, uris) -> uris
+                  | _ -> assert false
+                in
+                Cic.Var (uri, mk_subst uris)
+            | Cic.MutInd (uri, i, []) ->
+                let uris =
+                  (*match CicEnvironment.get_obj uri with*)
+                  match CicTypeChecker.typecheck uri with
+                  | Cic.InductiveDefinition (_, uris, _) -> uris
+                  | _ -> assert false
+                in
+                Cic.MutInd (uri, i, mk_subst uris)
+            | Cic.MutConstruct (uri, i, j, []) ->
+                let uris =
+                  (*match CicEnvironment.get_obj uri with*)
+                  match CicTypeChecker.typecheck uri with
+                  | Cic.InductiveDefinition (_, uris, _) -> uris
+                  | _ -> assert false
+                in
+                Cic.MutConstruct (uri, i, j, mk_subst uris)
+            | Cic.Meta _ | Cic.Implicit _ as t ->
 (*
-              prerr_endline (sprintf
-                "Warning: %s must be instantiated with _[%s] but we do not enforce it"
-                (CicPp.ppterm t)
-                (String.concat "; "
-                  (List.map
-                    (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
-                    subst)));
+                prerr_endline (sprintf
+                  "Warning: %s must be instantiated with _[%s] but we do not enforce it"
+                  (CicPp.ppterm t)
+                  (String.concat "; "
+                    (List.map
+                      (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
+                      subst)));
 *)
-              t
-          | _ ->
-              raise DisambiguateChoices.Invalid_choice))
+                t
+            | _ ->
+              raise DisambiguateChoices.Invalid_choice
+           with 
+             CicEnvironment.CircularDependency _ -> 
+               raise DisambiguateChoices.Invalid_choice))
     | CicAst.Implicit -> Cic.Implicit None
     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
     | CicAst.Meta (index, subst) ->
@@ -464,7 +472,7 @@ module Make (C: Callbacks) =
       in
       (* (3) test an interpretation filling with meta uninterpreted identifiers
        *)
-      let test_env current_env todo_dom =
+      let test_env current_env todo_dom univ = 
         let filled_env =
           List.fold_left
             (fun env item ->
@@ -476,55 +484,64 @@ module Make (C: Callbacks) =
             current_env todo_dom 
         in
         try
+          CicUniv.set_working univ; 
           let cic_term =
             interpretate ~context:disambiguate_context ~env:filled_env term
           in
-          refine metasenv context cic_term
+           let k = refine metasenv context cic_term in
+           let new_univ = CicUniv.get_working () in
+            (k , new_univ )
         with
-        | Try_again -> Uncertain
-        | DisambiguateChoices.Invalid_choice -> Ko
+        | Try_again -> Uncertain,univ 
+        | DisambiguateChoices.Invalid_choice -> Ko,univ 
       in
       (* (4) build all possible interpretations *)
-      let rec aux current_env todo_dom =
+      let rec aux current_env todo_dom base_univ =
         match todo_dom with
         | [] ->
-            (match test_env current_env [] with
-            | Ok (term, metasenv) -> [ current_env, metasenv, term ]
-            | Ko | Uncertain -> [])
+            (match test_env current_env [] base_univ with
+            | Ok (term, metasenv),new_univ -> 
+                               [ current_env, metasenv, term, new_univ ]
+            | Ko,_ | Uncertain,_ -> [])
         | item :: remaining_dom ->
             debug_print (sprintf "CHOOSED ITEM: %s"
-              (string_of_domain_item item));
+             (string_of_domain_item item));
             let choices = lookup_choices item in
-            let rec filter = function
+            let rec filter univ = function 
               | [] -> []
               | codomain_item :: tl ->
                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
                   let new_env =
                     Environment.add item codomain_item current_env
                   in
-                  (match test_env new_env remaining_dom with
-                  | Ok (term, metasenv) ->
+                  (match test_env new_env remaining_dom univ with
+                  | Ok (term, metasenv),new_univ ->
                       (match remaining_dom with
-                      | [] -> [ new_env, metasenv, term ]
-                      | _ -> aux new_env remaining_dom) @ filter tl
-                  | Uncertain ->
+                      | [] -> [ new_env, metasenv, term, new_univ ]
+                      | _ -> aux new_env remaining_dom new_univ )@ 
+                        filter univ tl
+                  | Uncertain,new_univ ->
                       (match remaining_dom with
                       | [] -> []
-                      | _ -> aux new_env remaining_dom) @ filter tl
-                  | Ko -> filter tl)
+                      | _ -> aux new_env remaining_dom new_univ )@ 
+                        filter univ tl
+                  | Ko,_ -> filter univ tl)
             in
-            filter choices
+            filter base_univ choices 
       in
-       match aux current_env todo_dom with
+       let base_univ = CicUniv.get_working () in
+      try
+       match aux current_env todo_dom base_univ with
        | [] -> raise NoWellTypedInterpretation
-       | [ _ ] as l ->
+       | [ e,me,t,u ] as l ->
            debug_print "UNA SOLA SCELTA";
-           l
+           CicUniv.set_working u;
+           [ e,me,t ]
        | l ->
            debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
            let choices =
              List.map
-               (fun (env, _, _) ->
+               (fun (env, _, _, _) ->
                  List.map
                    (fun domain_item ->
                      let description =
@@ -535,7 +552,17 @@ module Make (C: Callbacks) =
                l
            in
            let choosed = C.interactive_interpretation_choice choices in
-            List.map (List.nth l) choosed
-
+           let l' = List.map (List.nth l) choosed in
+           match l' with
+             [] -> assert false
+           | [e,me,t,u] -> 
+               CicUniv.set_working u;
+               (*CicUniv.print_working_graph ();*)
+               [e,me,t]
+           | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
+               List.map (fun (e,me,t,u) -> (e,me,t)) l'
+     with
+      CicEnvironment.CircularDependency s -> 
+        raise (Failure "e chi la becca sta CircularDependency?");
   end
 
index 8014a19404d99da98716962b039b203ef559e97d..e15186fdecdb489f437d50c91bbad63b3e54e00c 100644 (file)
@@ -38,6 +38,7 @@
 let cleanup_tmp = true;;
 
 let trust_obj = function uri -> true;;
+(*let trust_obj = function uri -> false;;*)
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -317,7 +318,9 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
+      CicUniv.directly_to_env_begin ();
       let obj = CicParser.obj_of_xml filename bodyfilename in
+      CicUniv.directly_to_env_end ();
        if cleanup_tmp then
         begin
          Unix.unlink filename ;
@@ -405,3 +408,11 @@ let in_cache uri =
   ignore (Cache.find_cooked uri);true
  with Not_found -> false
 ;;
+
+let add_type_checked_term uri obj =
+  match obj with 
+  Cic.Constant (s,(Some bo),ty,ul) ->
+    Cache.add_cooked ~key:uri obj
+  | _ -> assert false 
+  Cache.add_cooked 
+;;
index 615cdf9be37675fbab987ce27bb3257dcba8221f..e3def568e4bdeba80ae3b4ad147ed05eb6deaba2 100644 (file)
@@ -61,6 +61,9 @@ val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
+(* We need this in the Qed. *)
+val add_type_checked_term : UriManager.uri -> Cic.obj -> unit
+
 (* get_cooked_obj ~trust uri                                        *)
 (* returns the object if it is already type-checked or if it can be *)
 (* trusted (if [trust] = true and the trusting function accepts it) *)
index 36bfb28b19cd22c77c7471ec5343dab140f20861..140e4171287a73a4b1164f857306f31368bb2806 100644 (file)
@@ -127,6 +127,7 @@ let rec type_of_constant uri =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       CicUniv.directly_to_env_begin ();
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Constant (_,Some te,ty,_) ->
@@ -160,6 +161,7 @@ let rec type_of_constant uri =
             ("Unknown constant:" ^ U.string_of_uri uri))
        );
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -180,6 +182,7 @@ and type_of_variable uri =
      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
       CicLogger.log (`Start_type_checking uri) ;
+      CicUniv.directly_to_env_begin ();
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -190,6 +193,7 @@ and type_of_variable uri =
                 ("Unknown variable:" ^ U.string_of_uri uri))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        ty
    |  _ ->
@@ -518,8 +522,10 @@ and type_of_mutual_inductive_defs uri i =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       CicUniv.directly_to_env_begin ();
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
+       CicUniv.directly_to_env_end ();
        CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -543,8 +549,10 @@ and type_of_mutual_inductive_constr uri i j =
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        CicLogger.log (`Start_type_checking uri) ;
+       (*CicUniv.directly_to_env_begin ();*)
        check_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
+       (*CicUniv.directly_to_env_end ();*)
        CicLogger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked ~trust:false uri with
           CicEnvironment.CheckedObj cobj -> cobj
@@ -799,7 +807,7 @@ and guarded_by_destructors context n nn kl x safes =
         | Some (_,C.Def (bo,_)) ->
            guarded_by_destructors context m nn kl x safes
             (CicSubstitution.lift m bo)
-       | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+        | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
       )
    | C.Meta _
    | C.Sort _
@@ -1236,9 +1244,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
             C.Sort C.Prop
           | C.Sort C.Set  -> true
-         | C.Sort C.CProp -> true
+          | C.Sort C.CProp -> true
           | C.Sort (C.Type _) ->
-           (* TASSI: da verificare *)
+            (* TASSI: da verificare *)
              (match CicEnvironment.get_obj uri with
                  C.InductiveDefinition (itl,_,paramsno) ->
                   let (_,_,_,cl) = List.nth itl i in
@@ -1345,7 +1353,7 @@ and type_of_aux' metasenv context t =
           | Some (_,C.Def (bo,None)) ->
              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
              type_of_aux context (S.lift n bo)
-         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+          | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
         with
         _ ->
           raise (TypeCheckerFailure "unbound variable")
@@ -1366,8 +1374,8 @@ and type_of_aux' metasenv context t =
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
         if not (CicUniv.add_gt t' t ) then
-         assert false (* t' is fresh! an error in CicUniv *)
-       else
+          assert false (* t' is fresh! an error in CicUniv *)
+        else
           C.Sort (C.Type t')
       (* TASSI: CONSTRAINTS *)
     | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
@@ -1587,7 +1595,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
        List.rev
         (List.map
           (fun (n,ty,_) -> 
-           let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
+            let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
       in
        let len = List.length types in
         List.iter
@@ -1660,7 +1668,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
-        (* different from Coq manual!!! *)
+         (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
@@ -1670,7 +1678,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
        C.Sort (C.Type t')
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
-       C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+        C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
     | (C.Meta _, C.Sort _) -> t2'
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
@@ -1771,15 +1779,18 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
 *)
 ;;
 
+(* tassi FIXME: not sure where is this called... no history here... *)
 let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked ~trust:false uri with
-     CicEnvironment.CheckedObj _ -> ()
+  (*match CicEnvironment.is_type_checked ~trust:false uri with*)
+  match CicEnvironment.is_type_checked ~trust:true uri with
+     CicEnvironment.CheckedObj cobj -> cobj
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
       CicLogger.log (`Start_type_checking uri) ;
+      CicUniv.directly_to_env_begin ();
       (match uobj with
           C.Constant (_,Some te,ty,_) ->
            let _ = type_of ty in
@@ -1819,5 +1830,7 @@ let typecheck uri =
            check_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      CicLogger.log (`Type_checking_completed uri)
+      CicUniv.directly_to_env_end ();
+      CicLogger.log (`Type_checking_completed uri);
+      uobj
 ;;
index 95ee658c7de98b637cc10261e8b6317efa4d3959..3973c16c105515cf064d17cf39f6b8dba9ccca8d 100644 (file)
@@ -27,7 +27,7 @@
 exception TypeCheckerFailure of string
 exception AssertFailure of string
 
-val typecheck : UriManager.uri -> unit
+val typecheck : UriManager.uri -> Cic.obj
 
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL *)
 
index b3525d3182bcec3737d02c2883cd7402d1acf730..e8ea0769de76416d369ba4d5f5b9ff63ee0ed945 100644 (file)
@@ -162,8 +162,8 @@ and type_of_aux' metasenv context t =
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
      (* TASSI: CONSTRAINT *)
-    | C.Sort (C.Type t) ->
-        let t' = CicUniv.fresh() in
+    | C.Sort (C.Type t) -> 
+        let t' = CicUniv.fresh() in 
         if not (CicUniv.add_gt t' t ) then
          assert false (* t' is fresh! an error in CicUniv *)
        else
@@ -487,7 +487,7 @@ and type_of_aux' metasenv context t =
           C.Sort s2,subst,metasenv
      | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
-       let t' = CicUniv.fresh() in
+       let t' = CicUniv.fresh() in 
        if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
          assert false ; (* not possible, error in CicUniv *)
        C.Sort (C.Type t'),subst,metasenv
index 295c638b9224318fca9827a6545d96b2ea41b48c..9b42378112a1079cdc3146a09f25f2fa3ee7cf28 100644 (file)
@@ -14,10 +14,10 @@ http_getter_env.cmo: http_getter_const.cmi http_getter_logger.cmi \
     http_getter_misc.cmi http_getter_types.cmo http_getter_env.cmi 
 http_getter_env.cmx: http_getter_const.cmx http_getter_logger.cmx \
     http_getter_misc.cmx http_getter_types.cmx http_getter_env.cmi 
-http_getter_common.cmo: http_getter_env.cmi http_getter_misc.cmi \
-    http_getter_types.cmo http_getter_common.cmi 
-http_getter_common.cmx: http_getter_env.cmx http_getter_misc.cmx \
-    http_getter_types.cmx http_getter_common.cmi 
+http_getter_common.cmo: http_getter_env.cmi http_getter_logger.cmi \
+    http_getter_misc.cmi http_getter_types.cmo http_getter_common.cmi 
+http_getter_common.cmx: http_getter_env.cmx http_getter_logger.cmx \
+    http_getter_misc.cmx http_getter_types.cmx http_getter_common.cmi 
 http_getter_map.cmo: http_getter_map.cmi 
 http_getter_map.cmx: http_getter_map.cmi 
 http_getter_cache.cmo: http_getter_common.cmi http_getter_env.cmi \
index 3a60f60ac68568486637681f5bf5521e0a8d93d7..242671197dbba22a25c922740e9ff67ae09d7acc 100644 (file)
@@ -1,19 +1,23 @@
 filter_auto.cmi: newConstraints.cmi 
-proofEngineHelpers.cmi: proofEngineTypes.cmo 
-tacticals.cmi: proofEngineTypes.cmo 
-reductionTactics.cmi: proofEngineTypes.cmo 
-proofEngineStructuralRules.cmi: proofEngineTypes.cmo 
-primitiveTactics.cmi: proofEngineTypes.cmo 
-tacticChaser.cmi: proofEngineTypes.cmo 
-variousTactics.cmi: proofEngineTypes.cmo 
-introductionTactics.cmi: proofEngineTypes.cmo 
-eliminationTactics.cmi: proofEngineTypes.cmo 
-negationTactics.cmi: proofEngineTypes.cmo 
-equalityTactics.cmi: proofEngineTypes.cmo 
-discriminationTactics.cmi: proofEngineTypes.cmo 
-ring.cmi: proofEngineTypes.cmo 
-fourierR.cmi: proofEngineTypes.cmo 
-statefulProofEngine.cmi: proofEngineTypes.cmo 
+proofEngineHelpers.cmi: proofEngineTypes.cmi 
+tacticals.cmi: proofEngineTypes.cmi 
+reductionTactics.cmi: proofEngineTypes.cmi 
+proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
+primitiveTactics.cmi: proofEngineTypes.cmi 
+tacticChaser.cmi: proofEngineTypes.cmi 
+variousTactics.cmi: proofEngineTypes.cmi 
+introductionTactics.cmi: proofEngineTypes.cmi 
+eliminationTactics.cmi: proofEngineTypes.cmi 
+negationTactics.cmi: proofEngineTypes.cmi 
+equalityTactics.cmi: proofEngineTypes.cmi 
+discriminationTactics.cmi: proofEngineTypes.cmi 
+ring.cmi: proofEngineTypes.cmi 
+fourierR.cmi: proofEngineTypes.cmi 
+statefulProofEngine.cmi: proofEngineTypes.cmi 
+proofEngineTypes.cmo: proofEngineTypes.cmi 
+proofEngineTypes.cmx: proofEngineTypes.cmi 
+proofEngineTypes.cmo: proofEngineTypes.cmi 
+proofEngineTypes.cmx: proofEngineTypes.cmi 
 newConstraints.cmo: newConstraints.cmi 
 newConstraints.cmx: newConstraints.cmi 
 match_concl.cmo: newConstraints.cmi match_concl.cmi 
@@ -24,60 +28,58 @@ proofEngineReduction.cmo: proofEngineReduction.cmi
 proofEngineReduction.cmx: proofEngineReduction.cmi 
 proofEngineHelpers.cmo: proofEngineHelpers.cmi 
 proofEngineHelpers.cmx: proofEngineHelpers.cmi 
-newConstraints.cmo: newConstraints.cmi 
-newConstraints.cmx: newConstraints.cmi 
-match_concl.cmo: newConstraints.cmi match_concl.cmi 
-match_concl.cmx: newConstraints.cmx match_concl.cmi 
-tacticals.cmo: proofEngineTypes.cmo tacticals.cmi 
+tacticals.cmo: proofEngineTypes.cmi tacticals.cmi 
 tacticals.cmx: proofEngineTypes.cmx tacticals.cmi 
-reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi 
-reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi 
-proofEngineStructuralRules.cmo: proofEngineTypes.cmo \
+reductionTactics.cmo: proofEngineReduction.cmi proofEngineTypes.cmi \
+    reductionTactics.cmi 
+reductionTactics.cmx: proofEngineReduction.cmx proofEngineTypes.cmx \
+    reductionTactics.cmi 
+proofEngineStructuralRules.cmo: proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi 
 proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
     proofEngineStructuralRules.cmi 
 primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \
-    proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \
+    proofEngineTypes.cmi reductionTactics.cmi tacticals.cmi \
     primitiveTactics.cmi 
 primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
     proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
     primitiveTactics.cmi 
 tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \
-    primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi 
+    primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi 
 tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \
     primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi 
 variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \
-    proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi 
+    proofEngineTypes.cmi tacticChaser.cmi tacticals.cmi variousTactics.cmi 
 variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \
     proofEngineTypes.cmx tacticChaser.cmx tacticals.cmx variousTactics.cmi 
-introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \
+introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \
     introductionTactics.cmi 
 eliminationTactics.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \
-    tacticals.cmi eliminationTactics.cmi 
+    proofEngineTypes.cmi tacticals.cmi eliminationTactics.cmi 
 eliminationTactics.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \
-    tacticals.cmx eliminationTactics.cmi 
+    proofEngineTypes.cmx tacticals.cmx eliminationTactics.cmi 
 negationTactics.cmo: eliminationTactics.cmi primitiveTactics.cmi \
-    proofEngineTypes.cmo tacticals.cmi variousTactics.cmi negationTactics.cmi 
+    proofEngineTypes.cmi tacticals.cmi variousTactics.cmi negationTactics.cmi 
 negationTactics.cmx: eliminationTactics.cmx primitiveTactics.cmx \
     proofEngineTypes.cmx tacticals.cmx variousTactics.cmx negationTactics.cmi 
 equalityTactics.cmo: introductionTactics.cmi primitiveTactics.cmi \
     proofEngineHelpers.cmi proofEngineReduction.cmi \
-    proofEngineStructuralRules.cmi proofEngineTypes.cmo reductionTactics.cmi \
+    proofEngineStructuralRules.cmi proofEngineTypes.cmi reductionTactics.cmi \
     tacticals.cmi equalityTactics.cmi 
 equalityTactics.cmx: introductionTactics.cmx primitiveTactics.cmx \
     proofEngineHelpers.cmx proofEngineReduction.cmx \
     proofEngineStructuralRules.cmx proofEngineTypes.cmx reductionTactics.cmx \
     tacticals.cmx equalityTactics.cmi 
 discriminationTactics.cmo: eliminationTactics.cmi equalityTactics.cmi \
-    introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmo \
+    introductionTactics.cmi primitiveTactics.cmi proofEngineTypes.cmi \
     tacticals.cmi discriminationTactics.cmi 
 discriminationTactics.cmx: eliminationTactics.cmx equalityTactics.cmx \
     introductionTactics.cmx primitiveTactics.cmx proofEngineTypes.cmx \
     tacticals.cmx discriminationTactics.cmi 
 ring.cmo: eliminationTactics.cmi equalityTactics.cmi primitiveTactics.cmi \
-    proofEngineStructuralRules.cmi proofEngineTypes.cmo tacticals.cmi \
+    proofEngineStructuralRules.cmi proofEngineTypes.cmi tacticals.cmi \
     ring.cmi 
 ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \
     proofEngineStructuralRules.cmx proofEngineTypes.cmx tacticals.cmx \
@@ -85,10 +87,10 @@ ring.cmx: eliminationTactics.cmx equalityTactics.cmx primitiveTactics.cmx \
 fourier.cmo: fourier.cmi 
 fourier.cmx: fourier.cmi 
 fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \
-    proofEngineHelpers.cmi proofEngineTypes.cmo reductionTactics.cmi ring.cmi \
+    proofEngineHelpers.cmi proofEngineTypes.cmi reductionTactics.cmi ring.cmi \
     tacticals.cmi fourierR.cmi 
 fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \
     proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \
     tacticals.cmx fourierR.cmi 
-statefulProofEngine.cmo: proofEngineTypes.cmo statefulProofEngine.cmi 
+statefulProofEngine.cmo: proofEngineTypes.cmi statefulProofEngine.cmi 
 statefulProofEngine.cmx: proofEngineTypes.cmx statefulProofEngine.cmi 
index 0cf06c578f58d9016802fe4a179093886419df73..c837f2df8374dfb1bd1d51ff4157df86e843ad7e 100644 (file)
@@ -4,7 +4,7 @@ REQUIRES = \
        helm-cic_unification helm-mathql_interpreter helm-mathql_generator
 
 INTERFACE_FILES = \
-       newConstraints.mli match_concl.mli filter_auto.mli\
+       proofEngineTypes.mli newConstraints.mli match_concl.mli filter_auto.mli\
        proofEngineReduction.mli proofEngineHelpers.mli \
        tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
        primitiveTactics.mli tacticChaser.mli variousTactics.mli \
index dd2e68d09e8afcaf582ee88f10a7481cc63cfd0d..ceaccdcefaed715d9a636da8c34f222a1099447f 100644 (file)
@@ -25,7 +25,8 @@
 
 open HelmLibraryObjects
 
-let rec injection_tac ~term status = 
+let rec injection_tac ~term =
+ let injection_tac ~term status = 
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -34,6 +35,7 @@ let rec injection_tac ~term status =
    let _,metasenv,_,_ = proof in
     let _,context,_ = CicUtil.lookup_meta goal metasenv in
      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in  
+      ProofEngineTypes.apply_tactic
       (match termty with
           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
              when (U.eq equri Logic.eq_URI) -> (
@@ -43,7 +45,8 @@ let rec injection_tac ~term status =
                    match t1,t2 with
                       ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
-                         when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
+                         when (uri1 = uri2) && (typeno1 = typeno2) && 
+                             (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
                        (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac
                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
@@ -73,126 +76,132 @@ let rec injection_tac ~term status =
            )
         | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation")
       ) status
+ in 
+  ProofEngineTypes.mk_tactic (injection_tac ~term)
 
-
-and injection1_tac ~term ~i status = 
-let (proof, goal) = status in
-(* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module U = UriManager in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,_ = CicUtil.lookup_meta goal metasenv in
-     let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
-      match termty with (* an equality *)
-         (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-            when (U.eq equri Logic.eq_URI) -> (
-          match tty with (* some inductive type *)
-             (C.MutInd (turi,typeno,exp_named_subst))
-           | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
-prerr_endline ("XXXX term " ^ CicPp.ppterm term) ;
-prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ;
-prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
-prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
-prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
-              let t1',t2',consno = (* sono i due sottotermini che differiscono *)
-               match t1,t2 with
-                  ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
-                   (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
-                     when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *)
-                   (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
-                | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai")
-              in
-               let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in
-prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ;
-prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
-prerr_endline ("XXXX consno " ^ string_of_int consno) ;
-               let pattern =
-                     match (CicEnvironment.get_obj turi) with
-                        C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx)  ->
-                         let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
-                          let i_constr_id,_ = List.nth constructor_list (consno - 1) in
-                           List.map
-                            (function (id,cty) ->
-                              let reduced_cty = CicReduction.whd context cty in
-                               let rec aux t k =
-                                match t with
-                                   C.Prod (_,_,target) when (k <= nr_ind_params_dx) ->
-                                    aux target (k+1)
-                                 | C.Prod (binder,source,target) when (k > nr_ind_params_dx) ->
-                                   let binder' =
-                                     match binder with
-                                        C.Name b -> C.Name b
-                                      | C.Anonymous -> C.Name "y"
-                                    in
-                                     C.Lambda (binder',source,(aux target (k+1)))
-                                 | _ ->
-                                    let nr_param_constr = k - 1 - nr_ind_params_dx in
-                                     if (id = i_constr_id)
-                                      then C.Rel (nr_param_constr - i + 1)
-                                      else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *)
-                               in aux reduced_cty 1
-                            )
-                            constructor_list
-                      | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
+and injection1_tac ~term ~i = 
+ let injection1_tac ~term ~i status =
+  let (proof, goal) = status in
+  (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
+   let module C = Cic in
+   let module S = CicSubstitution in
+   let module U = UriManager in
+   let module P = PrimitiveTactics in
+   let module T = Tacticals in
+    let _,metasenv,_,_ = proof in
+     let _,context,_ = CicUtil.lookup_meta goal metasenv in
+      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
+       match termty with (* an equality *)
+          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
+             when (U.eq equri Logic.eq_URI) -> (
+           match tty with (* some inductive type *)
+              (C.MutInd (turi,typeno,exp_named_subst))
+            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
+ prerr_endline ("XXXX term " ^ CicPp.ppterm term) ;
+ prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ;
+ prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ;
+ prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ;
+ prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ;
+               let t1',t2',consno = (* sono i due sottotermini che differiscono *)
+                match t1,t2 with
+                   ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
+                    (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
+                      when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *)
+                    (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
+                 | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai")
                in
-prerr_endline ("XXXX cominciamo!") ;
-                T.thens 
-                 ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
-                 ~continuations:[
-                   T.then_ 
-                    ~start:(injection_tac ~term:(C.Rel 1))
-                    ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) 
-                   ;
-                   T.then_ 
-                    ~start:
-                      (fun status ->    
-                        let (proof, goal) = status in
-                        let _,metasenv,_,_ = proof in
-                         let _,context,gty = CicUtil.lookup_meta goal metasenv in
-prerr_endline ("XXXX goal " ^ string_of_int goal) ;
-prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
-prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
-prerr_endline ("XXXX change " ^ CicPp.ppterm (C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi, typeno, (C.Lambda ((C.Name "x"),(S.lift 1 tty),(S.lift 2 tty'))), (C.Rel 1), pattern)); t1])) ;
-                          let new_t1' = 
-                           match gty with 
-                              (C.Appl (C.MutInd (_,_,_)::arglist)) -> 
-                               List.nth arglist 1
-                            | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
-                          in
-prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ;
-                           P.change_tac
-                              ~what:new_t1'
-                              ~with_what:
-                                (C.Appl [
-                                  C.Lambda (
-                                   C.Name "x", tty,
-                                   C.MutCase (
-                                    turi, typeno,
-                                    (C.Lambda (
-                                     (C.Name "x"),
-                                     (S.lift 1 tty),
-                                     (S.lift 2 tty'))),
-                                    (C.Rel 1), pattern
-                                   )
-                                  );
-                                  t1]
-                                )
-                       status
-                      )
-                    ~continuation:
-                      (T.then_
-                        ~start:(EqualityTactics.rewrite_simpl_tac ~term)
-                        ~continuation:EqualityTactics.reflexivity_tac
-                      )
-                  ]     
-                 status
-           | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
-          )
-       | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
+                let tty' = (CicTypeChecker.type_of_aux' metasenv context t1') in
+ prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ;
+ prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ;
+ prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ;
+ prerr_endline ("XXXX consno " ^ string_of_int consno) ;
+                let pattern =
+                      match (CicEnvironment.get_obj turi) with
+                         C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx)  ->
+                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
+                           let i_constr_id,_ = List.nth constructor_list (consno - 1) in
+                            List.map
+                             (function (id,cty) ->
+                               let reduced_cty = CicReduction.whd context cty in
+                                let rec aux t k =
+                                 match t with
+                                    C.Prod (_,_,target) when (k <= nr_ind_params_dx) ->
+                                     aux target (k+1)
+                                  | C.Prod (binder,source,target) when (k > nr_ind_params_dx) ->
+                                   let binder' =
+                                      match binder with
+                                         C.Name b -> C.Name b
+                                       | C.Anonymous -> C.Name "y"
+                                     in
+                                      C.Lambda (binder',source,(aux target (k+1)))
+                                  | _ ->
+                                     let nr_param_constr = k - 1 - nr_ind_params_dx in
+                                      if (id = i_constr_id)
+                                       then C.Rel (nr_param_constr - i + 1)
+                                       else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda agguinto esternamente al case *)
+                                in aux reduced_cty 1
+                             )
+                             constructor_list
+                       | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
+                in
+ prerr_endline ("XXXX cominciamo!") ;
+                ProofEngineTypes.apply_tactic   
+                 (T.thens 
+                  ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
+                  ~continuations:[
+                    T.then_ 
+                     ~start:(injection_tac ~term:(C.Rel 1))
+                     ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) 
+                    ;
+                    T.then_ 
+                     ~start:(ProofEngineTypes.mk_tactic 
+                       (fun status ->    
+                         let (proof, goal) = status in
+                         let _,metasenv,_,_ = proof in
+                          let _,context,gty = CicUtil.lookup_meta goal metasenv in
+ prerr_endline ("XXXX goal " ^ string_of_int goal) ;
+ prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ;
+ prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ;
+ prerr_endline ("XXXX change " ^ CicPp.ppterm (C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi, typeno, (C.Lambda ((C.Name "x"),(S.lift 1 tty),(S.lift 2 tty'))), (C.Rel 1), pattern)); t1])) ;
+                           let new_t1' = 
+                            match gty with 
+                               (C.Appl (C.MutInd (_,_,_)::arglist)) -> 
+                                List.nth arglist 1
+                             | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
+                           in
+ prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ;
+                            ProofEngineTypes.apply_tactic 
+                            (P.change_tac
+                               ~what:new_t1'
+                               ~with_what:
+                                 (C.Appl [
+                                   C.Lambda (
+                                    C.Name "x", tty,
+                                    C.MutCase (
+                                     turi, typeno,
+                                     (C.Lambda (
+                                      (C.Name "x"),
+                                      (S.lift 1 tty),
+                                      (S.lift 2 tty'))),
+                                     (C.Rel 1), pattern
+                                    )
+                                   );
+                                   t1]
+                                 ))
+                        status
+                       ))
+                     ~continuation:
+                       (T.then_
+                         ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+                         ~continuation:EqualityTactics.reflexivity_tac
+                       )
+                   ])     
+                  status
+            | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
+           )
+        | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
+ in
+  ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;
 
 
@@ -202,7 +211,8 @@ exception TwoDifferentSubtermsFound of int
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
-let discriminate'_tac ~term status = 
+let discriminate'_tac ~term =
+ let discriminate'_tac ~term status = 
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -286,8 +296,9 @@ prerr_endline ("XXXX nth funzionano ") ;
                    in
 
                     let (proof',goals') = 
-                     EliminationTactics.elim_type_tac 
-                      ~term:(C.MutInd(Logic.false_URI,0,[]))
+                    ProofEngineTypes.apply_tactic 
+                      (EliminationTactics.elim_type_tac 
+                       ~term:(C.MutInd(Logic.false_URI,0,[])))
                       status 
                     in
                      (match goals' with
@@ -296,7 +307,8 @@ prerr_endline ("XXXX nth funzionano ") ;
                            let _,context',gty' =
                              CicUtil.lookup_meta goal' metasenv'
                            in
-                            T.then_
+                           ProofEngineTypes.apply_tactic
+                            (T.then_
                              ~start:
                               (P.change_tac 
                                ~what:gty' 
@@ -329,21 +341,26 @@ prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (Cic
                                  T.then_
                                    ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
-                              )
+                              ))
                              (proof',goal')
                        | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
                      )    
             | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
            )
        | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
+ in
+  ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
 ;;
 
-
-let discriminate_tac ~term status =
-  Tacticals.then_
-   ~start:(* (injection_tac ~term) *) Tacticals.id_tac
-   ~continuation:(discriminate'_tac ~term) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
+let discriminate_tac ~term = 
+ let discriminate_tac ~term status =
+  ProofEngineTypes.apply_tactic 
+  (Tacticals.then_
+    ~start:(* (injection_tac ~term) *) Tacticals.id_tac
+    ~continuation:(discriminate'_tac ~term)) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
    status
+ in
+  ProofEngineTypes.mk_tactic (discriminate_tac ~term)
 ;;
 
 
@@ -356,8 +373,8 @@ e' vera o no e lo risolve *)
 
 
 
-let compare_tac ~term status = Tacticals.id_tac status
-(*
+let compare_tac ~term = Tacticals.id_tac
+ (*
 (* term is in the form t1=t2; the tactic leaves two goals: in the first you have to          *)
 (* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2  *)
   let module C = Cic in
index 29aa1c4f1ed5157aea052a7f37f34946232745ce..1db11951fed63c9ac2383026412d9e859afe776a 100644 (file)
@@ -56,15 +56,18 @@ let induction_tac ~term status =
 ;;
 *)
 
-
-let elim_type_tac ~term status =
-  let module C = Cic in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   T.thens
-    ~start: (P.cut_tac term)
-    ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
-    status
+let elim_type_tac ~term =
+ let elim_type_tac ~term status =
+   let module C = Cic in
+   let module P = PrimitiveTactics in
+   let module T = Tacticals in
+    ProofEngineTypes.apply_tactic 
+     (T.thens
+      ~start: (P.cut_tac term)
+      ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ])
+     status
+ in
+  ProofEngineTypes.mk_tactic (elim_type_tac ~term)
 ;;
 
 
@@ -131,7 +134,8 @@ let call_back uris =
 ;;
 *)
 
-let decompose_tac ?(uris_choice_callback=(function l -> l)) term status =
+let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
+ let decompose_tac uris_choice_callback term status =
   let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
@@ -190,35 +194,39 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term status =
               | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) 
                  when (List.mem (uri,typeno,exp_named_subst) urilist) ->
                    warn ("elim " ^ CicPp.ppterm termty);
-                   T.then_ 
+                  ProofEngineTypes.apply_tactic 
+                   (T.then_ 
                       ~start:(P.elim_intros_simpl_tac ~term:term')
                       ~continuation:(
                         (* clear the hyp that has just been eliminated *)
-                        (fun status -> 
+                        ProofEngineTypes.mk_tactic (fun status -> 
                           let (proof, goal) = status in
                           let _,metasenv,_,_ = proof in
                            let _,context,_ = CicUtil.lookup_meta goal metasenv in
                             let new_context_len = List.length context in   
                              warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim));
                              let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
-                             T.then_ 
+                            ProofEngineTypes.apply_tactic
+                             (T.then_ 
                                 ~start:(
                                   if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) 
                                    then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
                                    else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
-                                ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)
+                                ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
                                 status
-                        ))
+                        )))
                       status
               | _ ->
                    let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in 
                     warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim));
                     elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status
          else (* no hyp to elim left in this goal *)
-          T.id_tac status
+          ProofEngineTypes.apply_tactic T.id_tac status
 
         in
          elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status
+ in
+  ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term)
 ;;
 
 
index 0e9f72b0f96b73d65ea5644a85dbdceda93913d6..a649d4a23e2df518e77f37f96662fd02a3fb718e 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-
-let rewrite_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const
-           (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
-         in
-          eq_ind_r,ty,t1,t2
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
+let rewrite_tac ~term:equality =
+ let rewrite_tac ~term:equality (proof,goal) =
+  let module C = Cic in
+  let module U = UriManager in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+    let eq_ind_r,ty,t1,t2 =
+     match CicTypeChecker.type_of_aux' metasenv context equality with
+        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
+         when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
+          let eq_ind_r =
+           C.Const
+            (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
+          in
+           eq_ind_r,ty,t1,t2
+      | _ ->
+        raise
+         (ProofEngineTypes.Fail
+           "Rewrite: the argument is not a proof of an equality")
     in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-          ((curi,metasenv',pbo,pty),goal)
+     let pred =
+      let gty' = CicSubstitution.lift 1 gty in
+      let t1' = CicSubstitution.lift 1 t1 in
+      let gty'' =
+       ProofEngineReduction.replace_lifting
+        ~equality:ProofEngineReduction.alpha_equivalence
+        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+      in
+       C.Lambda
+        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+          ty, gty'')
      in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
+     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+     let irl =CicMkImplicit.identity_relocation_list_for_metavariable context in
+     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+      let (proof',goals) =
+       ProofEngineTypes.apply_tactic 
+        (PrimitiveTactics.exact_tac
+         ~term:(C.Appl
+          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))        ((curi,metasenv',pbo,pty),goal)
+      in
+       assert (List.length goals = 0) ;
+       (proof',[fresh_meta])
+ in
+  ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
 ;;
 
 
-let rewrite_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
+let rewrite_simpl_tac ~term =
+ let rewrite_simpl_tac ~term status =
+  ProofEngineTypes.apply_tactic
+  (Tacticals.then_ 
+   ~start:(rewrite_tac ~term)
+   ~continuation:
+    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+   status
+ in
+  ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
 ;;
 
 
-let rewrite_back_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
-         in
-          eq_ind_r,ty,t2,t1
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
+let rewrite_back_tac ~term:equality =
+ let rewrite_back_tac equality (proof,goal) =
+  let module C = Cic in
+  let module U = UriManager in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+    let eq_ind_r,ty,t1,t2 =
+     match CicTypeChecker.type_of_aux' metasenv context equality with
+        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
+         when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
+          let eq_ind_r =
+           C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
+          in
+           eq_ind_r,ty,t2,t1
+      | _ ->
+        raise
+         (ProofEngineTypes.Fail
+           "Rewrite: the argument is not a proof of an equality")
     in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl =
-     CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-        ((curi,metasenv',pbo,pty),goal)
+     let pred =
+      let gty' = CicSubstitution.lift 1 gty in
+      let t1' = CicSubstitution.lift 1 t1 in
+      let gty'' =
+       ProofEngineReduction.replace_lifting
+        ~equality:ProofEngineReduction.alpha_equivalence
+        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+      in
+       C.Lambda
+        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+          ty, gty'')
      in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
-
+     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+     let irl =
+      CicMkImplicit.identity_relocation_list_for_metavariable context in
+     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+      let (proof',goals) =
+       ProofEngineTypes.apply_tactic
+        (PrimitiveTactics.exact_tac
+         ~term:(C.Appl
+          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))
+         ((curi,metasenv',pbo,pty),goal)
+      in
+       assert (List.length goals = 0) ;
+       (proof',[fresh_meta])
+ in
+  ProofEngineTypes.mk_tactic (rewrite_back_tac equality)
 ;;
 
 
-let rewrite_back_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_back_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
+let rewrite_back_simpl_tac ~term =
+ let rewrite_back_simpl_tac ~term status =
+  ProofEngineTypes.apply_tactic
+   (Tacticals.then_ 
+    ~start:(rewrite_back_tac ~term)
+    ~continuation:
+     (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+   status
+ in
+  ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
 ;;
 
-
-let replace_tac ~what ~with_what status =
+let replace_tac ~what ~with_what =
+ let replace_tac ~what ~with_what status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -147,7 +160,8 @@ let replace_tac ~what ~with_what status =
       try
       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
        then
-         T.thens
+        ProofEngineTypes.apply_tactic
+         (T.thens
           ~start:(
             P.cut_tac 
              (C.Appl [
@@ -161,10 +175,13 @@ let replace_tac ~what ~with_what status =
                ~continuation:(
                  ProofEngineStructuralRules.clear
                   ~hyp:(List.hd context)) ;
-            T.id_tac]
+            T.id_tac])
           status
        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
-       with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
+       with (Failure "hd") -> 
+            raise (ProofEngineTypes.Fail "Replace: empty context")
+ in
+  ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
 ;;
 
 
@@ -174,23 +191,28 @@ let reflexivity_tac =
   IntroductionTactics.constructor_tac ~n:1
 ;;
 
-
-let symmetry_tac (proof, goal) =
+let symmetry_tac =
+ let symmetry_tac (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
-         PrimitiveTactics.apply_tac (proof,goal)
-          ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
+        when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
+         ProofEngineTypes.apply_tactic 
+           (PrimitiveTactics.apply_tac 
+           ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))) 
+          (proof,goal)
 
       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
+ in
+  ProofEngineTypes.mk_tactic symmetry_tac
 ;;
 
-
-let transitivity_tac ~term status =
+let transitivity_tac ~term =
+ let transitivity_tac ~term status =
   let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
@@ -199,15 +221,19 @@ let transitivity_tac ~term status =
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = HelmLibraryObjects.Logic.eq_URI) ->
-         T.thens
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) 
+       when (uri = HelmLibraryObjects.Logic.eq_URI) ->
+         ProofEngineTypes.apply_tactic 
+        (T.thens
           ~start:(PrimitiveTactics.apply_tac
             ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
           ~continuations:
-            [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
+            [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac])
           status
 
       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
+ in
+  ProofEngineTypes.mk_tactic (transitivity_tac ~term)
 ;;
 
 
index f5cc890aa9d03873d3d7590f0777df32bd9fb1ec..3556a85f2e43e47cf2370cc324b0d89121cd26d2 100644 (file)
@@ -31,6 +31,7 @@ des in
 *)
 
 open Fourier
+open ProofEngineTypes
 
 
 let debug x = print_string ("____ "^x) ; flush stdout;;
@@ -569,7 +570,8 @@ let rational_to_real x =
 (* preuve que 0<n*1/d
 *)
 
-let tac_zero_inf_pos (n,d) status =
+let tac_zero_inf_pos (n,d) =
+ let tac_zero_inf_pos (n,d) status =
    (*let cste = pf_parse_constr gl in*)
    let pall str (proof,goal) t =
      debug ("tac "^str^" :\n" );
@@ -578,35 +580,40 @@ let tac_zero_inf_pos (n,d) status =
      debug ("th = "^ CicPp.ppterm t ^"\n"); 
      debug ("ty = "^ CicPp.ppterm ty^"\n"); 
    in
-   let tacn=ref 
-     (fun status -> pall "n0" status _Rlt_zero_1 ;
-       PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
-   let tacd=ref 
-     (fun status -> pall "d0" status _Rlt_zero_1 ;
-       PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
+   let tacn=ref (mk_tactic (fun status -> 
+        pall "n0" status _Rlt_zero_1 ;
+        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
+   let tacd=ref (mk_tactic (fun status -> 
+        pall "d0" status _Rlt_zero_1 ;
+        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
 
 
   for i=1 to n-1 do 
-       tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i) 
-        status _Rlt_zero_pos_plus1;
-         PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status) 
-          ~continuation:!tacn); 
+       tacn:=(Tacticals.then_ 
+        ~start:(mk_tactic (fun status -> 
+          pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1;
+          apply_tactic 
+           (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1)
+           status))
+        ~continuation:!tacn); 
   done;
   for i=1 to d-1 do
-       tacd:=(Tacticals.then_ ~start:(fun status -> pall "d" 
-        status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac 
-         ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd); 
+       tacd:=(Tacticals.then_ 
+        ~start:(mk_tactic (fun status -> 
+          pall "d" status _Rlt_zero_pos_plus1 ;
+          apply_tactic 
+           (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status)) 
+        ~continuation:!tacd); 
   done;
 
-
-
 debug("TAC ZERO INF POS\n");
-
-(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) 
-  ~continuations:[
-   !tacn ;
-   !tacd ] 
-  status)
+  apply_tactic 
+  (Tacticals.thens 
+    ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
+    ~continuations:[!tacn ;!tacd ] )
+  status
+ in
+  mk_tactic (tac_zero_inf_pos (n,d))
 ;;
 
 
@@ -614,30 +621,32 @@ debug("TAC ZERO INF POS\n");
 (* preuve que 0<=n*1/d
 *)
  
-let tac_zero_infeq_pos gl (n,d) status =
- (*let cste = pf_parse_constr gl in*)
- debug("inizio tac_zero_infeq_pos\n");
- let tacn = ref 
-  (*(if n=0 then
-    (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) 
-   else*)
-    (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
- (* ) *)
-  in
-  let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
-  for i=1 to n-1 do 
-      tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-       ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); 
-  done;
-  for i=1 to d-1 do
-      tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-       ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); 
-  done;
-  let r = 
-  (Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
-   ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in
-   debug("fine tac_zero_infeq_pos\n");
-   r
+let tac_zero_infeq_pos gl (n,d) =
+ let tac_zero_infeq_pos gl (n,d) status =
+  (*let cste = pf_parse_constr gl in*)
+  debug("inizio tac_zero_infeq_pos\n");
+  let tacn = ref 
+   (*(if n=0 then
+     (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) 
+    else*)
+     (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
+  (* ) *)
+   in
+   let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
+   for i=1 to n-1 do 
+       tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
+        ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); 
+   done;
+   for i=1 to d-1 do
+       tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
+        ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); 
+   done;
+   apply_tactic 
+    (Tacticals.thens 
+     ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) 
+     ~continuations:[!tacn;!tacd]) status 
+ in
+  mk_tactic (tac_zero_infeq_pos gl (n,d))
 ;;
 
 
@@ -645,75 +654,68 @@ let tac_zero_infeq_pos gl (n,d) status =
 (* preuve que 0<(-n)*(1/d) => False 
 *)
 
-let tac_zero_inf_false gl (n,d) status=
-  debug("inizio tac_zero_inf_false\n");
-    if n=0 then 
-     (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 status) in
-     debug("fine\n");
-     r)
-    else
-     (debug "2\n";let r = (Tacticals.then_ ~start:(
-       fun status -> 
+let tac_zero_inf_false gl (n,d) =
+ let tac_zero_inf_false gl (n,d) status =
+   if n=0 then 
+    apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
+   else
+    apply_tactic (Tacticals.then_ 
+     ~start:( mk_tactic (fun status -> 
        let (proof, goal) = status in
        let curi,metasenv,pbo,pty = proof in
        let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-         debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
-         ^ CicPp.ppterm ty ^"\n");
-       let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt status in
-       debug("!!!!!!!!!2\n");
-       r
-       )
-     ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in
-     debug("fine\n");
-     r
-     )
+        apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
+     ~continuation:(tac_zero_infeq_pos gl (-n,d))) 
+    status
+ in
+  mk_tactic (tac_zero_inf_false gl (n,d))
 ;;
 
 (* preuve que 0<=n*(1/d) => False ; n est negatif
 *)
 
-let tac_zero_infeq_false gl (n,d) status=
-let (proof, goal) = status in
-debug("stat tac_zero_infeq_false\n");
-let r = 
-     let curi,metasenv,pbo,pty = proof in
-     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-     
-     debug("faccio fold di " ^ CicPp.ppterm
-            (Cic.Appl
-              [_Rle ; _R0 ;
-               Cic.Appl
-                [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-              ]
-            ) ^ "\n") ;
-     debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
-     (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
-     Tacticals.then_
-      ~start:
-        (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-          ~also_in_hypotheses:false
-          ~term:
-            (Cic.Appl
-              [_Rle ; _R0 ;
-               Cic.Appl
-                [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-              ]
-            )
-        )
-      ~continuation:
-        (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
-          ~continuation:(tac_zero_inf_pos (-n,d))) status in
- debug("end tac_zero_infeq_false\n");
- r
-(*PORTING
- Tacticals.id_tac status
-*)
+let tac_zero_infeq_false gl (n,d) =
+ let tac_zero_infeq_false gl (n,d) status =
+  let (proof, goal) = status in
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  
+  debug("faccio fold di " ^ CicPp.ppterm
+         (Cic.Appl
+           [_Rle ; _R0 ;
+            Cic.Appl
+             [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+           ]
+         ) ^ "\n") ;
+  debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+  (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
+  apply_tactic 
+   (Tacticals.then_
+    ~start:
+      (ReductionTactics.fold_tac ~reduction:CicReduction.whd
+        ~also_in_hypotheses:false
+        ~term:
+          (Cic.Appl
+            [_Rle ; _R0 ;
+             Cic.Appl
+              [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+            ]
+          )
+      )
+    ~continuation:
+      (Tacticals.then_ 
+        ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+        ~continuation:(tac_zero_inf_pos (-n,d)))) 
+   status 
+ in
+  mk_tactic (tac_zero_infeq_false gl (n,d))
 ;;
 
 
 (* *********** ********** ******** ??????????????? *********** **************)
 
-let apply_type_tac ~cast:t ~applist:al (proof,goal) = 
+let apply_type_tac ~cast:t ~applist:al = 
+ let apply_type_tac ~cast:t ~applist:al (proof,goal) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
@@ -722,76 +724,73 @@ let apply_type_tac ~cast:t ~applist:al (proof,goal) =
   let metasenv' = (fresh_meta,context,t)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
-     PrimitiveTactics.apply_tac 
-      (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
-      ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
-       (proof',goal)
+     apply_tactic 
+      (PrimitiveTactics.apply_tac 
+       (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *)
+       ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *)
+      (proof',goal)
     in
      proof'',fresh_meta::goals
+ in
+  mk_tactic (apply_type_tac ~cast:t ~applist:al)
 ;;
 
-
-
-
-   
-let my_cut ~term:c (proof,goal)=
+let my_cut ~term:c =
+ let my_cut ~term:c (proof,goal) =
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-
-debug("my_cut di "^CicPp.ppterm c^"\n");
-
-
   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
   let irl =
    CicMkImplicit.identity_relocation_list_for_metavariable context in
   let metasenv' = (fresh_meta,context,c)::metasenv in
    let proof' = curi,metasenv',pbo,pty in
     let proof'',goals =
-     apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
-      CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] 
-       (proof',goal)
+     apply_tactic 
+      (apply_type_tac 
+       ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) 
+       ~applist:[Cic.Meta(fresh_meta,irl)])
+      (proof',goal)
     in
      (* We permute the generated goals to be consistent with Coq *)
      match goals with
         [] -> assert false
       | he::tl -> proof'',he::fresh_meta::tl
+ in
+  mk_tactic (my_cut ~term:c)
 ;;
 
-
 let exact = PrimitiveTactics.exact_tac;;
 
-let tac_use h status 
-let (proof, goal) = status in
-debug("Inizio TC_USE\n");
-let curi,metasenv,pbo,pty = proof in
-let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
-debug ("ty = "^ CicPp.ppterm ty^"\n"); 
-
-let res = 
-match h.htype with
-  "Rlt" -> exact ~term:h.hname status
-  |"Rle" -> exact ~term:h.hname status
-  |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-             ~term:_Rfourier_gt_to_lt) 
-              ~continuation:(exact ~term:h.hname)) status
-  |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-             ~term:_Rfourier_ge_to_le)
-              ~continuation:(exact ~term:h.hname)) status
-  |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-               ~term:_Rfourier_eqLR_to_le)
-                ~continuation:(exact ~term:h.hname)) status
-  |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac 
-               ~term:_Rfourier_eqRL_to_le)
-                ~continuation:(exact ~term:h.hname)) status
-  |_->assert false
-in
-debug("Fine TAC_USE\n");
-res
+let tac_use h = 
+ let tac_use h status = 
+  let (proof, goal) = status in
+  debug("Inizio TC_USE\n");
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); 
+  debug ("ty = "^ CicPp.ppterm ty^"\n");
+  apply_tactic 
+   (match h.htype with
+      "Rlt" -> exact ~term:h.hname 
+    | "Rle" -> exact ~term:h.hname 
+    | "Rgt" -> (Tacticals.then_ 
+                 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) 
+                 ~continuation:(exact ~term:h.hname)) 
+    | "Rge" -> (Tacticals.then_ 
+                 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
+                 ~continuation:(exact ~term:h.hname)) 
+    | "eqTLR" -> (Tacticals.then_ 
+                   ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
+                   ~continuation:(exact ~term:h.hname)) 
+    | "eqTRL" -> (Tacticals.then_ 
+                   ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
+                   ~continuation:(exact ~term:h.hname)) 
+    | _->assert false)
+   status
+ in
+  mk_tactic (tac_use h)
 ;;
 
-
-
 let is_ineq (h,t) =
     match t with
        Cic.Appl ( Cic.Const(u,boh)::next) ->
@@ -843,62 +842,64 @@ let rec filter_real_hyp context cont =
                           [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
   | a::next -> debug("  no\n"); filter_real_hyp next cont
 ;;*)
+
 let filter_real_hyp context _ =
   let rec filter_aux context num =
    match context with
-  [] -> []
-  | Some(Cic.Name(h),Cic.Decl(t))::next -> 
-                  (
-                  (*let n = find_in_context h cont in*)
-                debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
-                  [(Cic.Rel(num),t)] @ filter_aux next (num+1)
-                )
-  | a::next -> filter_aux next (num+1)
+     [] -> []
+   | Some(Cic.Name(h),Cic.Decl(t))::next -> 
+       [(Cic.Rel(num),t)] @ filter_aux next (num+1)
+   | a::next -> filter_aux next (num+1)
   in
-  filter_aux context 1
+   filter_aux context 1
 ;;
 
 
 (* lifts everithing at the conclusion level *)        
 let rec superlift c n=
   match c with
-  [] -> []
-  | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
-                  CicSubstitution.lift n a))] @ superlift next (n+1)
-  | Some(name,Cic.Def(a,None))::next   -> [Some(name,Cic.Def((
-                  CicSubstitution.lift n a),None))] @ superlift next (n+1)
-  | Some(name,Cic.Def(a,Some ty))::next   -> [Some(name,Cic.Def((
-                  CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
+    [] -> []
+  | Some(name,Cic.Decl(a))::next  -> 
+     [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1)
+  | Some(name,Cic.Def(a,None))::next -> 
+     [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1)
+  | Some(name,Cic.Def(a,Some ty))::next   -> 
+     [Some(name,
+      Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
+      ] @ superlift next (n+1)
   | _::next -> superlift next (n+1) (*??  ??*)
  
 ;;
 
-let equality_replace a b status =
-debug("inizio EQ\n");
- let module C = Cic in
-  let proof,goal = status in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-   let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
-   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-   let irl =
-    CicMkImplicit.identity_relocation_list_for_metavariable context in
-   let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
-debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
-   let (proof,goals) =
-    EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
+let equality_replace a b =
+ let equality_replace a b status =
+ debug("inizio EQ\n");
+  let module C = Cic in
+   let proof,goal = status in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+    let irl =
+     CicMkImplicit.identity_relocation_list_for_metavariable context in
+    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+ debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
+    let (proof,goals) = apply_tactic 
+     (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)))
      ((curi,metasenv',pbo,pty),goal)
-   in
-   let new_goals = fresh_meta::goals in
-debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
-  ^string_of_int( List.length goals)^"+ meta\n");
-    (proof,new_goals)
+    in
+    let new_goals = fresh_meta::goals in
+ debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
+   ^string_of_int( List.length goals)^"+ meta\n");
+     (proof,new_goals)
+ in 
+  mk_tactic (equality_replace a b)
 ;;
 
 let tcl_fail a (proof,goal) =
-        match a with
-        1 -> raise (ProofEngineTypes.Fail "fail-tactical")
-        |_-> (proof,[goal])
+  match a with
+    1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+  | _ -> (proof,[goal])
 ;;
 
 (* Galla: moved in variousTactics.ml 
@@ -935,13 +936,13 @@ let contradiction_tac (proof,goal)=
 let rec fourier (s_proof,s_goal)=
   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
   let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
-  debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
+  debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
   debug_pcontext s_context;
 
   let fhyp = String.copy "new_hyp_for_fourier" in 
    
-(* here we need to negate the thesis, but to do this we need to apply the right
-theoreme,so let's parse our thesis *)
+(* here we need to negate the thesis, but to do this we need to apply the 
+   right theoreme,so let's parse our thesis *)
   
   let th_to_appl = ref _Rfourier_not_le_gt in   
   (match s_ty with
@@ -961,11 +962,12 @@ theoreme,so let's parse our thesis *)
 
    (* now let's change our thesis applying the th and put it with hp *) 
 
-   let proof,gl =
-    Tacticals.then_ 
-     ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
-     ~continuation:(PrimitiveTactics.intros_tac ())
-     (s_proof,s_goal) in
+   let proof,gl = apply_tactic 
+    (Tacticals.then_ 
+      ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+      ~continuation:(PrimitiveTactics.intros_tac ()))
+    (s_proof,s_goal) 
+   in
    let goal = if List.length gl = 1 then List.hd gl 
                                     else failwith "a new goal" in
 
@@ -977,7 +979,6 @@ theoreme,so let's parse our thesis *)
    let curi,metasenv,pbo,pty = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 
-
    (* now we want to convert hp to inequations, but first we must lift
       everyting to thesis level, so that a variable has the save Rel(n) 
       in each hp ( needed by ineq1_of_term ) *)
@@ -997,7 +998,6 @@ theoreme,so let's parse our thesis *)
   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
                         with _-> ())
               hyps;
-
             
   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
          " disequazioni\n");
@@ -1057,28 +1057,26 @@ theoreme,so let's parse our thesis *)
        debug "inizio a costruire tac1\n";
        Fourier.print_rational(c1);
           
-       let tac1=ref ( fun status -> 
-         if h1.hstrict then 
+       let tac1=ref ( mk_tactic (fun status -> 
+         apply_tactic
+          (if h1.hstrict then 
            (Tacticals.thens 
-             ~start:(
-              fun status -> 
+             ~start:(mk_tactic (fun status -> 
               debug ("inizio t1 strict\n");
               let curi,metasenv,pbo,pty = proof in
               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); 
               debug ("ty = "^ CicPp.ppterm ty^"\n"); 
-              PrimitiveTactics.apply_tac ~term:_Rfourier_lt status)
-            ~continuations:[tac_use h1;tac_zero_inf_pos  
-             (rational_to_fraction c1)] 
-            status
-           )
-           else 
+              apply_tactic 
+               (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status))
+            ~continuations:[tac_use h1;
+              tac_zero_inf_pos (rational_to_fraction c1)])
+          else 
            (Tacticals.thens 
              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
              ~continuations:[tac_use h1;tac_zero_inf_pos
-              (rational_to_fraction c1)] status
-           )
-         )
+              (rational_to_fraction c1)]))
+          status))
                    
        in
        s:=h1.hstrict;
@@ -1087,45 +1085,39 @@ theoreme,so let's parse our thesis *)
            (if h.hstrict then 
              (debug("tac1 1\n");
              tac1:=(Tacticals.thens 
-               ~start:(PrimitiveTactics.apply_tac 
-                ~term:_Rfourier_lt_lt)
+               ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt)
                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
-                (rational_to_fraction c)])
-             )
-           else 
+                (rational_to_fraction c)]))
+            else 
              (debug("tac1 2\n");
              Fourier.print_rational(c1);
              tac1:=(Tacticals.thens 
-              ~start:(
-                fun status -> 
+              ~start:(mk_tactic (fun status -> 
                 debug("INIZIO TAC 1 2\n");
                 let curi,metasenv,pbo,pty = proof in
                 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); 
                 debug ("ty = "^ CicPp.ppterm ty^"\n"); 
-                PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le status)
+                apply_tactic 
+                 (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le) 
+                 status))
               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos 
-                (rational_to_fraction c)])
-             )
-           )
-         else 
+                (rational_to_fraction c)])))
+          else 
            (if h.hstrict then 
              (debug("tac1 3\n");
              tac1:=(Tacticals.thens 
                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos  
-                (rational_to_fraction c)])
-             )
-           else 
+                (rational_to_fraction c)]))
+            else 
              (debug("tac1 4\n");
              tac1:=(Tacticals.thens 
                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos  
-                (rational_to_fraction c)])
-             )
-           )
-         );
-         s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
+                (rational_to_fraction c)]))));
+         s:=(!s)||(h.hstrict)) (* end fun -> *)
+         lutil;(*end List.iter*)
                      
        let tac2 = 
          if sres then 
@@ -1135,48 +1127,46 @@ theoreme,so let's parse our thesis *)
        in
        tac:=(Tacticals.thens 
          ~start:(my_cut ~term:ineq) 
-         ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_  
-           ~start:(fun status ->
+         ~continuations:[Tacticals.then_  
+           ~start:( mk_tactic (fun status ->
              let (proof, goal) = status in
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-             PrimitiveTactics.change_tac ~what:ty 
-              ~with_what:(Cic.Appl [ _not; ineq]) status)
+             apply_tactic 
+              (PrimitiveTactics.change_tac ~what:ty 
+                ~with_what:(Cic.Appl [ _not; ineq])) 
+              status))
            ~continuation:(Tacticals.then_ 
              ~start:(PrimitiveTactics.apply_tac ~term:
                (if sres then _Rnot_lt_lt else _Rnot_le_le))
              ~continuation:(Tacticals.thens 
-               ~start:( 
-                 fun status ->
-                 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
-                 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc 
+               ~start:(mk_tactic (fun status ->
+                 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^
+                  CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
+                 let r = apply_tactic 
+                 (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc) 
                   status
                  in
                  (match r with (p,gl) -> 
                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
-                 r)
+                 r))
                ~continuations:[(Tacticals.thens 
-                 ~start:(
-                   fun status ->
-                   let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in
+                 ~start:(mk_tactic (fun status ->
+                   let r = apply_tactic 
+                   (equality_replace (Cic.Appl[_Rinv;_R1]) _R1) 
+                   status 
+                  in
                    (match r with (p,gl) ->
                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
-                   r)
+                   r))
                  ~continuations:
-                   [PrimitiveTactics.apply_tac ~term:_Rinv_R1
-                 ;Tacticals.try_tactics 
-                   ~tactics:[ "ring", (fun status -> 
-                                        debug("begin RING\n");
-                                        let r = Ring.ring_tac  status in
-                                        debug ("end RING\n");
-                                        r)
-                        ; "id", Tacticals.id_tac] 
-                 ])
+                   [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
+                   Tacticals.try_tactics 
+                     ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
+                   ])
                ;(*Tacticals.id_tac*)
                 Tacticals.then_ 
-                 ~start:
-                  (
-                  fun status ->
+                 ~start:(mk_tactic (fun status ->
                    let (proof, goal) = status in
                    let curi,metasenv,pbo,pty = proof in
                    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -1187,11 +1177,11 @@ theoreme,so let's parse our thesis *)
                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
                      |_ -> assert false)
                    in
-                   let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 status in
+                   let r = apply_tactic 
+                    (PrimitiveTactics.change_tac ~what:ty ~with_what:w1) 
+                    status in
                    debug("fine MY_CHNGE\n");
-                   r
-                   
-                  ) 
+                   r)) 
                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
          ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
 
@@ -1199,12 +1189,12 @@ theoreme,so let's parse our thesis *)
   |_-> assert false); (*match res*)
   debug ("finalmente applico tac\n");
   (
-  let r = !tac (proof,goal) in
+  let r = apply_tactic !tac (proof,goal) in
   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
   
   ) 
 ;;
 
-let fourier_tac (proof,goal) = fourier (proof,goal);;
+let fourier_tac = mk_tactic fourier
 
 
index 9751b2b7478fdf0d05dc74ea092fbfc1b60c6774..f6283cf680644e6bb9db6413d1d3bf746a7fe816 100644 (file)
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let constructor_tac ~n (proof, goal) =
+let fake_constructor_tac ~n (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
@@ -31,14 +31,17 @@ let constructor_tac ~n (proof, goal) =
      match (R.whd context ty) with
         (C.MutInd (uri, typeno, exp_named_subst))
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
-         PrimitiveTactics.apply_tac 
-          ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-          (proof, goal)
+         ProofEngineTypes.apply_tactic (
+          PrimitiveTactics.apply_tac 
+           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)))
+           (proof, goal)
       | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
 ;;
 
-let exists_tac status = constructor_tac ~n:1 status ;;
-let split_tac status = constructor_tac ~n:1 status ;;
-let left_tac status = constructor_tac ~n:1 status ;;
-let right_tac status = constructor_tac ~n:2 status ;;
+let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n)
+
+let exists_tac  = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let split_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let left_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let right_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:2) ;;
 
index 65fe892fa61a09aa161226ddc135708ff0a52d21..a4b7d9ba844c8868bea0ecc973107b71e67c493d 100644 (file)
@@ -23,8 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let absurd_tac ~term status =
+let absurd_tac ~term =
+ let absurd_tac ~term status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -32,31 +32,41 @@ let absurd_tac ~term status =
    let _,metasenv,_,_ = proof in
     let _,context,ty = CicUtil.lookup_meta goal metasenv in
      if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
-      then P.apply_tac 
-              ~term:(C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; term ; ty]) status
+      then ProofEngineTypes.apply_tactic 
+       (P.apply_tac 
+        ~term:(
+         C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
+                term ; ty])
+       ) 
+       status
       else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+ in
+  ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
-
-let contradiction_tac status =
+let contradiction_tac =
+ let contradiction_tac status =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    try
-    T.then_
+    ProofEngineTypes.apply_tactic (
+     T.then_
       ~start:(P.intros_tac ())
       ~continuation:(
-        T.then_
+        T.then_
            ~start:
              (EliminationTactics.elim_type_tac 
                 ~term:
                   (C.MutInd (HelmLibraryObjects.Logic.false_URI, 0, [])))
-           ~continuation: VariousTactics.assumption_tac)
+           ~continuation: VariousTactics.assumption_tac))
     status
    with 
     (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption")
     (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *)
+ in 
+  ProofEngineTypes.mk_tactic contradiction_tac
 ;;
 
 (* Questa era in fourierR.ml
index 388ac2056ef6fb560480aa43ac91403a7b4a9404..d26de444714f312904017658a0fe7739dd82ea7b 100644 (file)
@@ -334,231 +334,247 @@ let apply_tac ~term (proof, goal) =
 
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
-let apply_tac ~term status =
+let apply_tac ~term =
+ let apply_tac ~term status =
   try
     apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with CicUnification.UnificationFailure _ as e ->
     raise (Fail (Printexc.to_string e))
+ in
+  mk_tactic (apply_tac ~term)
 
-let intros_tac
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
- (proof, goal)
-=
- let module C = Cic in
- let module R = CicReduction in
-  let (_,metasenv,_,_) = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-   let newmeta = new_meta_of_proof ~proof in
-    let (context',ty',bo') =
-     lambda_abstract metasenv context newmeta ty mk_fresh_name_callback
-    in
-     let (newproof, _) =
-       subst_meta_in_proof proof metano bo' [newmeta,context',ty']
-     in
-      (newproof, [newmeta])
-
-let cut_tac
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term (proof, goal)
-=
- let module C = Cic in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-   let newmeta1 = new_meta_of_proof ~proof in
-   let newmeta2 = newmeta1 + 1 in
-   let fresh_name =
-    mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
-   let context_for_newmeta1 =
-    (Some (fresh_name,C.Decl term))::context in
-   let irl1 =
-    CicMkImplicit.identity_relocation_list_for_metavariable
-     context_for_newmeta1
-   in
-   let irl2 =
-     CicMkImplicit.identity_relocation_list_for_metavariable context
-   in
-    let newmeta1ty = CicSubstitution.lift 1 ty in
-    let bo' =
-     C.Appl
-      [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
-       C.Meta (newmeta2,irl2)]
-    in
-     let (newproof, _) =
-      subst_meta_in_proof proof metano bo'
-       [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
-     in
-      (newproof, [newmeta1 ; newmeta2])
-
-let letin_tac
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- term (proof, goal)
-=
- let module C = Cic in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-   let _ = CicTypeChecker.type_of_aux' metasenv context term in
+let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()=
+ let intros_tac
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) ()
+  (proof, goal)
+ =
+  let module C = Cic in
+  let module R = CicReduction in
+   let (_,metasenv,_,_) = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let newmeta = new_meta_of_proof ~proof in
+     let (context',ty',bo') =
+      lambda_abstract metasenv context newmeta ty mk_fresh_name_callback
+     in
+      let (newproof, _) =
+        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
+      in
+       (newproof, [newmeta])
+ in
+  mk_tactic (intros_tac ~mk_fresh_name_callback ())
+  
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) term=
+ let cut_tac
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
+  term (proof, goal)
+ =
+  let module C = Cic in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let newmeta1 = new_meta_of_proof ~proof in
+    let newmeta2 = newmeta1 + 1 in
     let fresh_name =
-     mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
-    let context_for_newmeta =
-     (Some (fresh_name,C.Def (term,None)))::context in
-    let irl =
+     mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
+    let context_for_newmeta1 =
+     (Some (fresh_name,C.Decl term))::context in
+    let irl1 =
      CicMkImplicit.identity_relocation_list_for_metavariable
-      context_for_newmeta
+      context_for_newmeta1
+    in
+    let irl2 =
+      CicMkImplicit.identity_relocation_list_for_metavariable context
     in
-     let newmetaty = CicSubstitution.lift 1 ty in
-     let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
+     let newmeta1ty = CicSubstitution.lift 1 ty in
+     let bo' =
+      C.Appl
+       [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
+        C.Meta (newmeta2,irl2)]
+     in
       let (newproof, _) =
-        subst_meta_in_proof
-          proof metano bo'[newmeta,context_for_newmeta,newmetaty]
+       subst_meta_in_proof proof metano bo'
+        [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
       in
-       (newproof, [newmeta])
+       (newproof, [newmeta1 ; newmeta2])
+ in
+  mk_tactic (cut_tac ~mk_fresh_name_callback term)
 
-  (** functional part of the "exact" tactic *)
-let exact_tac ~term (proof, goal) =
- (* Assumption: the term bo must be closed in the current context *)
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let module T = CicTypeChecker in
- let module R = CicReduction in
- if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
-  begin
-   let (newproof, metasenv') =
-     subst_meta_in_proof proof metano term [] in
-   (newproof, [])
-  end
- else
-  raise (Fail "The type of the provided term is not the one expected.")
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name) term=
+ let letin_tac
+  ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
+  term (proof, goal)
+ =
+  let module C = Cic in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let _ = CicTypeChecker.type_of_aux' metasenv context term in
+     let newmeta = new_meta_of_proof ~proof in
+     let fresh_name =
+      mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
+     let context_for_newmeta =
+      (Some (fresh_name,C.Def (term,None)))::context in
+     let irl =
+      CicMkImplicit.identity_relocation_list_for_metavariable
+       context_for_newmeta
+     in
+      let newmetaty = CicSubstitution.lift 1 ty in
+      let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
+       let (newproof, _) =
+         subst_meta_in_proof
+           proof metano bo'[newmeta,context_for_newmeta,newmetaty]
+       in
+        (newproof, [newmeta])
+ in
+  mk_tactic (letin_tac ~mk_fresh_name_callback term)
 
+  (** functional part of the "exact" tactic *)
+let exact_tac ~term =
+ let exact_tac ~term (proof, goal) =
+  (* Assumption: the term bo must be closed in the current context *)
+  let (_,metasenv,_,_) = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  let module T = CicTypeChecker in
+  let module R = CicReduction in
+  if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
+   begin
+    let (newproof, metasenv') =
+      subst_meta_in_proof proof metano term [] in
+    (newproof, [])
+   end
+  else
+   raise (Fail "The type of the provided term is not the one expected.")
+ in
+  mk_tactic (exact_tac ~term)
 
 (* not really "primitive" tactics .... *)
-
-let elim_tac ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module U = UriManager in
- let module R = CicReduction in
- let module C = Cic in
-  let (curi,metasenv,_,_) = proof in
-  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-   let termty = T.type_of_aux' metasenv context term in
-   let uri,exp_named_subst,typeno,args =
-    match termty with
-       C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
-     | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
-         (uri,exp_named_subst,typeno,args)
-     | _ -> raise NotAnInductiveTypeToEliminate
-   in
-    let eliminator_uri =
-     let buri = U.buri_of_uri uri in
-     let name = 
-      match CicEnvironment.get_obj uri with
-         C.InductiveDefinition (tys,_,_) ->
-          let (name,_,_,_) = List.nth tys typeno in
-           name
-       | _ -> assert false
-     in
-     let ext =
-      match T.type_of_aux' metasenv context ty with
-         C.Sort C.Prop -> "_ind"
-       | C.Sort C.Set  -> "_rec"
-       | C.Sort C.CProp -> "_rec"
-       | C.Sort (C.Type _)-> "_rect" (* TASSI *)
-       | _ -> assert false
-     in
-      U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
+let elim_tac ~term = 
+ let elim_tac ~term (proof, goal) =
+  let module T = CicTypeChecker in
+  let module U = UriManager in
+  let module R = CicReduction in
+  let module C = Cic in
+   let (curi,metasenv,_,_) = proof in
+   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+    let termty = T.type_of_aux' metasenv context term in
+    let uri,exp_named_subst,typeno,args =
+     match termty with
+        C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+      | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+          (uri,exp_named_subst,typeno,args)
+      | _ -> raise NotAnInductiveTypeToEliminate
     in
-     let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
-      let ety = T.type_of_aux' metasenv context eliminator_ref in
-      let newmeta = new_meta_of_proof ~proof in
-       let (econclusion,newmetas,arguments,lastmeta) =
-         new_metasenv_for_apply newmeta proof context ety
-       in
-        (* Here we assume that we have only one inductive hypothesis to *)
-        (* eliminate and that it is the last hypothesis of the theorem. *)
-        (* A better approach would be fingering the hypotheses in some  *)
-        (* way.                                                         *)
-        let meta_of_corpse =
-         let (_,canonical_context,_) =
-           CicUtil.lookup_meta (lastmeta - 1) newmetas
-         in
-          let irl =
-           CicMkImplicit.identity_relocation_list_for_metavariable
-            canonical_context
-          in
-           Cic.Meta (lastmeta - 1, irl)
-        in
-        let newmetasenv = newmetas @ metasenv in
-        let subst1,newmetasenv' =
-         CicUnification.fo_unif newmetasenv context term meta_of_corpse
+     let eliminator_uri =
+      let buri = U.buri_of_uri uri in
+      let name = 
+       match CicEnvironment.get_obj uri with
+          C.InductiveDefinition (tys,_,_) ->
+           let (name,_,_,_) = List.nth tys typeno in
+            name
+        | _ -> assert false
+      in
+      let ext =
+       match T.type_of_aux' metasenv context ty with
+          C.Sort C.Prop -> "_ind"
+        | C.Sort C.Set  -> "_rec"
+        | C.Sort C.CProp -> "_rec"
+        | C.Sort (C.Type _)-> "_rect" (* TASSI *)
+        | _ -> assert false
+      in
+       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
+     in
+      let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
+       let ety = T.type_of_aux' metasenv context eliminator_ref in
+       let newmeta = new_meta_of_proof ~proof in
+        let (econclusion,newmetas,arguments,lastmeta) =
+          new_metasenv_for_apply newmeta proof context ety
         in
-         let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in
-          (* The conclusion of our elimination principle is *)
-          (*  (?i farg1 ... fargn)                         *)
-          (* The conclusion of our goal is ty. So, we can   *)
-          (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
-          (* a new ty equal to (P farg1 ... fargn). Now     *)
-          (* ?i can be instantiated with P and we are ready *)
-          (* to refine the term.                            *)
-          let emeta, fargs =
-           match ueconclusion with
-              C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
-            | C.Meta (emeta,_) -> emeta,[]
-            | _ -> raise NotTheRightEliminatorShape
+         (* Here we assume that we have only one inductive hypothesis to *)
+         (* eliminate and that it is the last hypothesis of the theorem. *)
+         (* A better approach would be fingering the hypotheses in some  *)
+         (* way.                                                         *)
+         let meta_of_corpse =
+          let (_,canonical_context,_) =
+            CicUtil.lookup_meta (lastmeta - 1) newmetas
           in
-           let ty' = CicMetaSubst.apply_subst subst1 ty in
-           let eta_expanded_ty =
-(*CSC: newmetasenv' era metasenv ??????????? *)
-            List.fold_left (eta_expand newmetasenv' context) ty' fargs
+           let irl =
+            CicMkImplicit.identity_relocation_list_for_metavariable
+             canonical_context
            in
-            let subst2,newmetasenv'' =
-(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
-da subst1!!!! Dovrei rimuoverle o sono innocue?*)
-             CicUnification.fo_unif
-              newmetasenv' context ueconclusion eta_expanded_ty
+            Cic.Meta (lastmeta - 1, irl)
+         in
+         let newmetasenv = newmetas @ metasenv in
+         let subst1,newmetasenv' =
+          CicUnification.fo_unif newmetasenv context term meta_of_corpse
+         in
+          let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in
+           (* The conclusion of our elimination principle is *)
+           (*  (?i farg1 ... fargn)                         *)
+           (* The conclusion of our goal is ty. So, we can   *)
+           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
+           (* a new ty equal to (P farg1 ... fargn). Now     *)
+           (* ?i can be instantiated with P and we are ready *)
+           (* to refine the term.                            *)
+           let emeta, fargs =
+            match ueconclusion with
+               C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
+             | C.Meta (emeta,_) -> emeta,[]
+             | _ -> raise NotTheRightEliminatorShape
+           in
+            let ty' = CicMetaSubst.apply_subst subst1 ty in
+            let eta_expanded_ty =
+ (*CSC: newmetasenv' era metasenv ??????????? *)
+             List.fold_left (eta_expand newmetasenv' context) ty' fargs
             in
-             let in_subst_domain i =
-              let eq_to_i = function (j,_) -> i=j in
-               List.exists eq_to_i subst1 ||
-               List.exists eq_to_i subst2
+             let subst2,newmetasenv'' =
+ (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
+ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
+              CicUnification.fo_unif
+               newmetasenv' context ueconclusion eta_expanded_ty
              in
-              (* When unwinding the META that corresponds to the elimination *)
-              (* predicate (which is emeta), we must also perform one-step   *)
-              (* beta-reduction. apply_subst doesn't need the context. Hence *)
-              (* the underscore.                                             *)
-              let apply_subst _ t =
-               let t' = CicMetaSubst.apply_subst subst1 t in
-                CicMetaSubst.apply_subst_reducing
-                 (Some (emeta,List.length fargs)) subst2 t'
+              let in_subst_domain i =
+               let eq_to_i = function (j,_) -> i=j in
+                List.exists eq_to_i subst1 ||
+                List.exists eq_to_i subst2
               in
-                let old_uninstantiatedmetas,new_uninstantiatedmetas =
-                 classify_metas newmeta in_subst_domain apply_subst
-                  newmetasenv''
-                in
-                 let arguments' = List.map (apply_subst context) arguments in
-                  let bo' = Cic.Appl (eliminator_ref::arguments') in
-                   let newmetasenv''' =
-                    new_uninstantiatedmetas@old_uninstantiatedmetas
-                   in
-                    let (newproof, newmetasenv'''') =
-                     (* When unwinding the META that corresponds to the *)
-                     (* elimination predicate (which is emeta), we must *)
-                     (* also perform one-step beta-reduction.           *)
-                     (* The only difference w.r.t. apply_subst is that  *)
-                     (* we also substitute metano with bo'.             *)
-                     (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
-                     (*CSC: no?                                              *)
-                     let apply_subst' t =
-                      let t' = CicMetaSubst.apply_subst subst1 t in
-                       CicMetaSubst.apply_subst_reducing
-                        (Some (emeta,List.length fargs))
-                        ((metano,bo')::subst2) t'
-                     in
-                      subst_meta_and_metasenv_in_proof
-                        proof metano apply_subst' newmetasenv'''
+               (* When unwinding the META that corresponds to the elimination *)
+               (* predicate (which is emeta), we must also perform one-step   *)
+               (* beta-reduction. apply_subst doesn't need the context. Hence *)
+               (* the underscore.                                             *)
+               let apply_subst _ t =
+                let t' = CicMetaSubst.apply_subst subst1 t in
+                 CicMetaSubst.apply_subst_reducing
+                  (Some (emeta,List.length fargs)) subst2 t'
+               in
+                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
+                  classify_metas newmeta in_subst_domain apply_subst
+                   newmetasenv''
+                 in
+                  let arguments' = List.map (apply_subst context) arguments in
+                   let bo' = Cic.Appl (eliminator_ref::arguments') in
+                    let newmetasenv''' =
+                     new_uninstantiatedmetas@old_uninstantiatedmetas
                     in
-                     (newproof,
-                      List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+                     let (newproof, newmetasenv'''') =
+                      (* When unwinding the META that corresponds to the *)
+                      (* elimination predicate (which is emeta), we must *)
+                      (* also perform one-step beta-reduction.           *)
+                      (* The only difference w.r.t. apply_subst is that  *)
+                      (* we also substitute metano with bo'.             *)
+                      (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
+                      (*CSC: no?                                              *)
+                      let apply_subst' t =
+                       let t' = CicMetaSubst.apply_subst subst1 t in
+                        CicMetaSubst.apply_subst_reducing
+                         (Some (emeta,List.length fargs))
+                         ((metano,bo')::subst2) t'
+                      in
+                       subst_meta_and_metasenv_in_proof
+                         proof metano apply_subst' newmetasenv'''
+                     in
+                      (newproof,
+                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+ in
+  mk_tactic (elim_tac ~term)
 ;;
 
 (* The simplification is performed only on the conclusion *)
@@ -577,35 +593,38 @@ exception NotConvertible
 (*CSC: while [what] can have a richer context (because of binders)           *)
 (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
-let change_tac ~what ~with_what (proof, goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  (* are_convertible works only on well-typed terms *)
-  ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
-  if CicReduction.are_convertible context what with_what then
-   begin
-    let replace =
-     ProofEngineReduction.replace
-      ~equality:(==) ~what:[what] ~with_what:[with_what]
-    in
-    let ty' = replace ty in
-    let context' =
-     List.map
-      (function
-          Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None))
-        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-        | None -> None
-        | Some (_,Cic.Def (_,Some _)) -> assert false
-      ) context
-    in
-     let metasenv' = 
+let change_tac ~what ~with_what =
+ let change_tac ~what ~with_what (proof, goal) =
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+   (* are_convertible works only on well-typed terms *)
+   ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
+   if CicReduction.are_convertible context what with_what then
+    begin
+     let replace =
+      ProofEngineReduction.replace
+       ~equality:(==) ~what:[what] ~with_what:[with_what]
+     in
+     let ty' = replace ty in
+     let context' =
       List.map
        (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
+           Some (name,Cic.Def (t,None))->Some (name,Cic.Def ((replace t),None))
+         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
+         | None -> None
+         | Some (_,Cic.Def (_,Some _)) -> assert false
+       ) context
      in
-      (curi,metasenv',pbo,pty), [metano]
-   end
-  else
-   raise (ProofEngineTypes.Fail "Not convertible")
+      let metasenv' = 
+       List.map
+        (function
+            (n,_,_) when n = metano -> (metano,context',ty')
+          | _ as t -> t
+        ) metasenv
+      in
+       (curi,metasenv',pbo,pty), [metano]
+    end
+   else
+    raise (ProofEngineTypes.Fail "Not convertible")
+ in
+  mk_tactic (change_tac ~what ~with_what)
index 20b0f21c9f307f0c8f9f05042f3f6aa4147f3f8d..e8956944528197c456992eb72d1dae5e777701a3 100644 (file)
 
 open ProofEngineTypes
 
-let clearbody ~hyp (proof, goal) =
- let module C = Cic in
-  match hyp with
-     None -> assert false
-   | Some (_, C.Def (_, Some _)) -> assert false
-   | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
-   | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
-      let curi,metasenv,pbo,pty = proof in
-       let metano,_,_ = CicUtil.lookup_meta goal metasenv in
-        let string_of_name =
-         function
-            C.Name n -> n
-          | C.Anonymous -> "_"
-        in
-        let metasenv' =
-         List.map
-          (function
-              (m,canonical_context,ty) when m = metano ->
-                let canonical_context' =
-                 List.fold_right
-                  (fun entry context ->
-                    match entry with
-                       t when t == hyp_to_clear_body ->
-                        let cleared_entry =
-                         let ty =
-                          CicTypeChecker.type_of_aux' metasenv context term
+let clearbody ~hyp = 
+ let clearbody ~hyp (proof, goal) =
+  let module C = Cic in
+   match hyp with
+      None -> assert false
+    | Some (_, C.Def (_, Some _)) -> assert false
+    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
+    | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
+       let curi,metasenv,pbo,pty = proof in
+        let metano,_,_ = CicUtil.lookup_meta goal metasenv in
+         let string_of_name =
+          function
+             C.Name n -> n
+           | C.Anonymous -> "_"
+         in
+         let metasenv' =
+          List.map
+           (function
+               (m,canonical_context,ty) when m = metano ->
+                 let canonical_context' =
+                  List.fold_right
+                   (fun entry context ->
+                     match entry with
+                        t when t == hyp_to_clear_body ->
+                         let cleared_entry =
+                          let ty =
+                           CicTypeChecker.type_of_aux' metasenv context term
+                          in
+                           Some (n_to_clear_body, Cic.Decl ty)
+                         in
+                          cleared_entry::context
+                      | None -> None::context
+                      | Some (n,C.Decl t)
+                      | Some (n,C.Def (t,None)) ->
+                         let _ =
+                          try
+                           CicTypeChecker.type_of_aux' metasenv context t
+                          with
+                           _ ->
+                             raise
+                              (Fail
+                                ("The correctness of hypothesis " ^
+                                 string_of_name n ^
+                                 " relies on the body of " ^
+                                 string_of_name n_to_clear_body)
+                              )
                          in
-                          Some (n_to_clear_body, Cic.Decl ty)
-                        in
-                         cleared_entry::context
-                     | None -> None::context
-                     | Some (n,C.Decl t)
-                     | Some (n,C.Def (t,None)) ->
-                        let _ =
-                         try
-                          CicTypeChecker.type_of_aux' metasenv context t
-                         with
-                          _ ->
-                            raise
-                             (Fail
-                               ("The correctness of hypothesis " ^
-                                string_of_name n ^
-                                " relies on the body of " ^
-                                string_of_name n_to_clear_body)
-                             )
-                        in
-                         entry::context
-                     | Some (_,Cic.Def (_,Some _)) -> assert false
-                  ) canonical_context []
-                in
-                 let _ =
-                  try
-                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                  with
-                   _ ->
-                    raise
-                     (Fail
-                      ("The correctness of the goal relies on the body of " ^
-                       string_of_name n_to_clear_body))
+                          entry::context
+                      | Some (_,Cic.Def (_,Some _)) -> assert false
+                   ) canonical_context []
                  in
-                  m,canonical_context',ty
-            | t -> t
-          ) metasenv
-        in
-         (curi,metasenv',pbo,pty), [goal]
+                  let _ =
+                   try
+                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+                   with
+                    _ ->
+                     raise
+                      (Fail
+                       ("The correctness of the goal relies on the body of " ^
+                        string_of_name n_to_clear_body))
+                  in
+                   m,canonical_context',ty
+             | t -> t
+           ) metasenv
+         in
+          (curi,metasenv',pbo,pty), [goal]
+ in
+  mk_tactic (clearbody ~hyp)
 
-let clear ~hyp:hyp_to_clear (proof, goal) =
- let module C = Cic in
-  match hyp_to_clear with
-     None -> assert false
-   | Some (n_to_clear, _) ->
-      let curi,metasenv,pbo,pty = proof in
-       let metano,context,ty =
-        CicUtil.lookup_meta goal metasenv
-       in
-        let string_of_name =
-         function
-            C.Name n -> n
-          | C.Anonymous -> "_"
+let clear ~hyp =
+ let clear ~hyp:hyp_to_clear (proof, goal) =
+  let module C = Cic in
+   match hyp_to_clear with
+      None -> assert false
+    | Some (n_to_clear, _) ->
+       let curi,metasenv,pbo,pty = proof in
+        let metano,context,ty =
+         CicUtil.lookup_meta goal metasenv
         in
-        let metasenv' =
-         List.map
-          (function
-              (m,canonical_context,ty) when m = metano ->
-                let canonical_context' =
-                 List.fold_right
-                  (fun entry context ->
-                    match entry with
-                       t when t == hyp_to_clear -> None::context
-                     | None -> None::context
-                     | Some (_,Cic.Def (_,Some _)) -> assert false
-                     | Some (n,C.Decl t)
-                     | Some (n,C.Def (t,None)) ->
-                        let _ =
-                         try
-                          CicTypeChecker.type_of_aux' metasenv context t
-                         with
-                          _ ->
-                            raise
-                             (Fail
-                               ("Hypothesis " ^
-                                string_of_name n ^
-                                " uses hypothesis " ^
-                                string_of_name n_to_clear)
-                             )
-                        in
-                         entry::context
-                  ) canonical_context []
-                in
-                 let _ =
-                  try
-                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                  with
-                   _ ->
-                    raise
-                     (Fail
-                      ("Hypothesis " ^ string_of_name n_to_clear ^
-                       " occurs in the goal"))
+         let string_of_name =
+          function
+             C.Name n -> n
+           | C.Anonymous -> "_"
+         in
+         let metasenv' =
+          List.map
+           (function
+               (m,canonical_context,ty) when m = metano ->
+                 let canonical_context' =
+                  List.fold_right
+                   (fun entry context ->
+                     match entry with
+                        t when t == hyp_to_clear -> None::context
+                      | None -> None::context
+                      | Some (_,Cic.Def (_,Some _)) -> assert false
+                      | Some (n,C.Decl t)
+                      | Some (n,C.Def (t,None)) ->
+                         let _ =
+                          try
+                           CicTypeChecker.type_of_aux' metasenv context t
+                          with
+                           _ ->
+                             raise
+                              (Fail
+                                ("Hypothesis " ^
+                                 string_of_name n ^
+                                 " uses hypothesis " ^
+                                 string_of_name n_to_clear)
+                              )
+                         in
+                          entry::context
+                   ) canonical_context []
                  in
-                  m,canonical_context',ty
-            | t -> t
-          ) metasenv
-        in
-         (curi,metasenv',pbo,pty), [goal]
-
+                  let _ =
+                   try
+                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
+                   with
+                    _ ->
+                     raise
+                      (Fail
+                       ("Hypothesis " ^ string_of_name n_to_clear ^
+                        " occurs in the goal"))
+                  in
+                   m,canonical_context',ty
+             | t -> t
+           ) metasenv
+         in
+          (curi,metasenv',pbo,pty), [goal]
+ in
+  mk_tactic (clear ~hyp)
index 3e0a12e4e406a0e689bead48c5da8be38e0b9a54..ac0713bd057dc364c44a193f71cb1b475a14e564 100644 (file)
@@ -38,9 +38,22 @@ type status = proof * goal
   (** an unfinished proof with the optional current goal *)
 type tactic = status -> proof * goal list
 
+  (** creates an opaque tactic from a status->proof*goal list function *)
+let mk_tactic t = t
+
   (** tactic failure *)
 exception Fail of string
 
+  (** 
+    calls the opaque tactic on the status, restoring the original 
+    universe graph if the tactic Fails
+  *)
+let apply_tactic t status = 
+  let saved_univ = CicUniv.get_working() in
+  try 
+    t status
+  with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+
   (** constraint: the returned value will always be constructed by Cic.Name **)
 type mk_fresh_name_type =
  Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli
new file mode 100644 (file)
index 0000000..c58b729
--- /dev/null
@@ -0,0 +1,49 @@
+(* Copyright (C) 2002, 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://cs.unibo.it/helm/.
+ *)
+
+  (**
+    current proof (proof uri * metas * (in)complete proof * term to be prooved)
+  *)
+type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
+  (** current goal, integer index *)
+type goal = int
+type status = proof * goal
+
+  (**
+    a tactic: make a transition from one status to another one or, usually,
+    raise a "Fail" (@see Fail) exception in case of failure
+  *)
+  (** an unfinished proof with the optional current goal *)
+type tactic 
+val mk_tactic: (status -> proof * goal list) -> tactic
+
+  (** tactic failure *)
+exception Fail of string
+
+val apply_tactic: tactic -> status ->  proof * goal list
+  
+  (** constraint: the returned value will always be constructed by Cic.Name **)
+type mk_fresh_name_type =
+ Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
index 80cb3306a18b79a4c08e1c8b40e9625014f86c9e..d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6 100644 (file)
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+open ProofEngineTypes
+
 (*
 let reduction_tac ~reduction (proof,goal) =
  let curi,metasenv,pbo,pty = proof in
@@ -89,41 +91,52 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
       (curi,metasenv',pbo,pty), [metano]
 ;;
 
-let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
-let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
-let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
+let simpl_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl 
+  ~also_in_hypotheses ~terms);;
 
-let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let term' = reduction context term in
-   (* We don't know if [term] is a subterm of [ty] or a subterm of *)
-   (* the type of one metavariable. So we replace it everywhere.   *)
-   (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
-   (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
-   let replace =
-    ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
-   in
-    let ty' = replace ty in
-    let metasenv' =
-     let context' =
-      if also_in_hypotheses then
+let reduce_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce
+  ~also_in_hypotheses ~terms);;
+  
+let whd_tac ~also_in_hypotheses ~terms = 
+ mk_tactic ( reduction_tac ~reduction:CicReduction.whd 
+  ~also_in_hypotheses ~terms);;
+
+let fold_tac ~reduction ~also_in_hypotheses ~term =
+ let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+   let term' = reduction context term in
+    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+    (* the type of one metavariable. So we replace it everywhere.   *)
+    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
+    let replace =
+     ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
+    in
+     let ty' = replace ty in
+     let metasenv' =
+      let context' =
+       if also_in_hypotheses then
+        List.map
+         (function
+             Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
+           | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
+           | None -> None
+           | Some (_,Cic.Def (_,Some _)) -> assert false
+         ) context
+       else
+        context
+      in
        List.map
         (function
-            Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
-          | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
-          | None -> None
-          | Some (_,Cic.Def (_,Some _)) -> assert false
-        ) context
-      else
-       context
+            (n,_,_) when n = metano -> (metano,context',ty')
+          | _ as t -> t
+        ) metasenv
+      
      in
-      List.map
-       (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
-     
-    in
-     (curi,metasenv',pbo,pty), [metano]
+      (curi,metasenv',pbo,pty), [metano]
+ in
+  mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term)
 ;;
index e2de0459193e91339b562f4f3a27075781585d78..cf6950c4be9776a7d4de1ad309c1a29d4da8b6e2 100644 (file)
@@ -389,11 +389,15 @@ let elim_type_tac ~term status =
     @param term term to cut
     @param proof term used to prove second subgoal generated by elim_type
   *)
-let elim_type2_tac ~term ~proof status =
+let elim_type2_tac ~term ~proof =
+ let elim_type2_tac ~term ~proof status =
   let module E = EliminationTactics in
   warn "in Ring.elim_type2";
-  Tacticals.thens ~start:(E.elim_type_tac ~term)
-   ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
+  ProofEngineTypes.apply_tactic 
+   (Tacticals.thens ~start:(E.elim_type_tac ~term)
+    ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
+ in
+  ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
 
 (* Galla: spostata in variousTactics.ml
   (**
@@ -423,7 +427,8 @@ let lift ~n (a,b,c,d,e,f,g,h) =
     @param count number of hypotheses to remove
     @param status current proof engine status
   *)
-let purge_hyps_tac ~count status =
+let purge_hyps_tac ~count =
+ let purge_hyps_tac ~count status =
   let module S = ProofEngineStructuralRules in
   let (proof, goal) = status in
   let rec aux n context status =
@@ -432,7 +437,8 @@ let purge_hyps_tac ~count status =
     | (0, _) -> status
     | (n, hd::tl) ->
         aux (n-1) tl
-         (status_of_single_goal_tactic_result (S.clear ~hyp:hd status))
+         (status_of_single_goal_tactic_result 
+         (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in
@@ -440,6 +446,8 @@ let purge_hyps_tac ~count status =
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
       proof',[goal']
+ in
+  ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
 
 (** THE TACTIC! *)
 
@@ -447,6 +455,7 @@ let purge_hyps_tac ~count status =
     Ring tactic, does associative and commutative rewritings in Reals ring
     @param status current proof engine status
   *)
 let ring_tac status =
   let (proof, goal) = status in
   warn "in Ring tactic";
@@ -467,8 +476,8 @@ let ring_tac status =
            t2; t2'; t2''; t2'_eq_t2'']);
       try
         let new_hyps = ref 0 in  (* number of new hypotheses created *)
-        Tacticals.try_tactics
-          status
+       ProofEngineTypes.apply_tactic 
+         (Tacticals.try_tactics
           ~tactics:[
             "reflexivity", EqualityTactics.reflexivity_tac ;
             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -483,15 +492,17 @@ let ring_tac status =
                  ] ;
                 t1'_eq_t1''
                ]) ;
-            "elim_type eqt su t1 ...", (fun status ->
+            "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
                 if not (are_convertible context t1'' t1) then begin
                   warn "t1'' and t1 are NOT CONVERTIBLE";
                   let newstatus =
-                    elim_type2_tac  (* 1st elim_type use *)
-                      status ~proof:t1'_eq_t1''
-                      ~term:(Cic.Appl [eqt; r; t1''; t1])
+                   ProofEngineTypes.apply_tactic 
+                    (elim_type2_tac  (* 1st elim_type use *)
+                      ~proof:t1'_eq_t1''
+                      ~term:(Cic.Appl [eqt; r; t1''; t1]))
+                   status 
                   in
                    incr new_hyps; (* elim_type add an hyp *)
                    match newstatus with
@@ -506,8 +517,8 @@ let ring_tac status =
                 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
               in
               let status'' =
-                Tacticals.try_tactics (* try to solve 1st subgoal *)
-                  status'
+              ProofEngineTypes.apply_tactic
+                (Tacticals.try_tactics (* try to solve 1st subgoal *)
                   ~tactics:[
                     "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
                     "exact sym_eqt su t2 ...",
@@ -521,15 +532,18 @@ let ring_tac status =
                             ] ;
                            t2'_eq_t2''
                           ]) ;
-                    "elim_type eqt su t2 ...", (fun status ->
+                    "elim_type eqt su t2 ...", 
+                    ProofEngineTypes.mk_tactic (fun status ->
                       let status' =
                         let context = context_of_status status in
                         if not (are_convertible context t2'' t2) then begin
                           warn "t2'' and t2 are NOT CONVERTIBLE";
                           let newstatus =
-                            elim_type2_tac  (* 2nd elim_type use *)
-                              status ~proof:t2'_eq_t2''
-                              ~term:(Cic.Appl [eqt; r; t2''; t2])
+                           ProofEngineTypes.apply_tactic 
+                             (elim_type2_tac  (* 2nd elim_type use *)
+                              ~proof:t2'_eq_t2''
+                              ~term:(Cic.Appl [eqt; r; t2''; t2]))
+                            status
                           in
                           incr new_hyps; (* elim_type add an hyp *)
                           match newstatus with
@@ -542,12 +556,16 @@ let ring_tac status =
                       in
                       try (* try to solve main goal *)
                         warn "trying reflexivity ....";
-                        EqualityTactics.reflexivity_tac status'
+                        ProofEngineTypes.apply_tactic 
+                        EqualityTactics.reflexivity_tac status'
                       with (Fail _) ->  (* leave conclusion to the user *)
                         warn "reflexivity failed, solution's left as an ex :-)";
-                        purge_hyps_tac ~count:!new_hyps status')]
+                        ProofEngineTypes.apply_tactic 
+                        (purge_hyps_tac ~count:!new_hyps) status')])
+                 status'       
               in
-              status'')]
+              status'')])
+        status      
       with (Fail s) ->
         raise (Fail ("Ring failure: " ^ s))
     end
@@ -555,9 +573,12 @@ let ring_tac status =
     assert false
 
   (* wrap ring_tac catching GoalUnringable and raising Fail *)
+
 let ring_tac status =
   try
     ring_tac status
   with GoalUnringable ->
     raise (Fail "goal unringable")
 
+let ring_tac = ProofEngineTypes.mk_tactic ring_tac
+
index 1c970249c78faed48ced7d1df0d7692d6cb7cf91..94710c412e034972ab65212f0497dd48098e7871 100644 (file)
@@ -183,7 +183,7 @@ class ['a] status
       let old_internal_status = self#internal_status in
       let (new_proof, new_goals) =
         try
-          tactic (_proof, self#active_goal)
+          ProofEngineTypes.apply_tactic tactic (_proof, self#active_goal)
         with exn -> raise (Tactic_failure exn)
       in
       _proof <- new_proof;
index f9c7feae7012589438ca3171d48d5e8407a4a6d1..c8217e78660b33a24a94f08a1fcdee6f18eb31f9 100644 (file)
@@ -75,10 +75,10 @@ match list_of_must with
            if 
             let time = Unix.gettimeofday() in
             (try
-             ignore
+             ignore(ProofEngineTypes.apply_tactic 
                (PrimitiveTactics.apply_tac
                  ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                          (MQueryMisc.cic_textual_parser_uri_of_string uri))
+                          (MQueryMisc.cic_textual_parser_uri_of_string uri)))
                  status);
               let time1 = Unix.gettimeofday() in
                 prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
@@ -179,9 +179,9 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
             try
               (m,
               (prerr_endline ("STO APPLICANDO " ^ uri);
-               (PrimitiveTactics.apply_tac
+               (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
                   ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                           (MQueryMisc.cic_textual_parser_uri_of_string uri))
+                           (MQueryMisc.cic_textual_parser_uri_of_string uri)))
                   status)))::tl'
             (* with ProofEngineTypes.Fail _ -> tl' *)
             (* patch to cover CSC's exportation bug *)
index 8d4eb891e049a8e0601daabf7d8289898f20bf02..5ea64913d0debbeacac87bcd4673a060f134c88c 100644 (file)
@@ -42,7 +42,10 @@ let warn s =
 
   (* not a tactical, but it's used only here (?) *)
 
-let id_tac (proof,goal) = (proof,[goal])
+let id_tac = 
+ let tac (proof,goal) = (proof,[goal])
+ in 
+  mk_tactic tac
 
 
   (**
@@ -54,13 +57,14 @@ let id_tac (proof,goal) = (proof,[goal])
     Galla: is this exactly Coq's "First"?
 
   *)
-let rec try_tactics ~(tactics: (string * tactic) list) status =
+let try_tactics ~tactics =
+ let rec try_tactics ~(tactics: (string * tactic) list) status =
   warn "in Tacticals.try_tactics";
   match tactics with
   | (descr, tac)::tactics ->
       warn ("Tacticals.try_tactics IS TRYING " ^ descr);
       (try
-        let res = tac status in
+        let res = apply_tactic tac status in
         warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
         res
        with
@@ -76,30 +80,35 @@ let rec try_tactics ~(tactics: (string * tactic) list) status =
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
   | [] -> raise (Fail "try_tactics: no tactics left")
+ in
+  mk_tactic (try_tactics ~tactics)
 
 
-
-let thens ~start ~continuations status =
- let (proof,new_goals) = start status in
+let thens ~start ~continuations =
+ let thens ~start ~continuations status =
+ let (proof,new_goals) = apply_tactic start status in
   try
    List.fold_left2
     (fun (proof,goals) goal tactic ->
-      let (proof',new_goals') = tactic (proof,goal) in
+      let (proof',new_goals') = apply_tactic tactic (proof,goal) in
        (proof',goals@new_goals')
     ) (proof,[]) new_goals continuations
   with
    Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+ in
+  mk_tactic (thens ~start ~continuations )
 
 
-
-let then_ ~start ~continuation status =
- let (proof,new_goals) = start status in
+let then_ ~start ~continuation =
+ let then_ ~start ~continuation status =
+ let (proof,new_goals) = apply_tactic start status in
   List.fold_left
    (fun (proof,goals) goal ->
-     let (proof',new_goals') = continuation (proof,goal) in
+     let (proof',new_goals') = apply_tactic continuation (proof,goal) in
       (proof',goals@new_goals')
    ) (proof,[]) new_goals
-
+ in
+  mk_tactic (then_ ~start ~continuation)
 
 (* Galla *)
 (* si suppone che tutte le tattiche sollevino solamente Fail? *)
@@ -111,9 +120,10 @@ let then_ ~start ~continuation status =
 (* When <tactic> generates more than one goal, you have a tree of
    application on the tactic, repeat_tactic works in depth on this tree *)
 
-let rec repeat_tactic ~tactic status =
+let repeat_tactic ~tactic =
+ let rec repeat_tactic ~tactic status =
   warn "in repeat_tactic";
-  try let (proof, goallist) = tactic status in
+  try let (proof, goallist) = apply_tactic tactic status in
    let rec step proof goallist =
     match goallist with
        [] -> (proof, [])
@@ -126,25 +136,29 @@ let rec repeat_tactic ~tactic status =
   with 
    (Fail _) as e ->
     warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    id_tac status
+    apply_tactic id_tac status
+ in 
+  mk_tactic (repeat_tactic ~tactic)
 ;;
 
 
 
 (* This tries to apply tactic n times *)
-
-let rec do_tactic ~n ~tactic status =
+let do_tactic ~n ~tactic =
+ let rec do_tactic ~n ~tactic status =
   warn "in do_tactic";
   try 
    let (proof, goallist) = 
-    if (n>0) then tactic status 
-             else id_tac status in
-(*             else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *)
+    if (n>0) then apply_tactic tactic status 
+             else apply_tactic id_tac status in
+(*             else (proof, []) in *)
+(* perche' non va bene questo? stessa questione di ##### ? *)
    let rec step proof goallist =
     match goallist with
        [] -> (proof, [])
      | head::tail -> 
-        let (proof', goallist') = do_tactic ~n:(n-1) ~tactic (proof, head) in
+        let (proof', goallist') = 
+        do_tactic ~n:(n-1) ~tactic (proof, head) in
         let (proof'', goallist'') = step proof' tail in
          proof'', goallist'@goallist''
    in
@@ -152,48 +166,57 @@ let rec do_tactic ~n ~tactic status =
   with 
    (Fail _) as e ->
     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    id_tac status
+    apply_tactic id_tac status
+ in
+  mk_tactic (do_tactic ~n ~tactic)
 ;;
 
 
 
 (* This applies tactic and catches its possible failure *)
-
-let rec try_tactic ~tactic status =
+let try_tactic ~tactic =
+ let rec try_tactic ~tactic status =
   warn "in Tacticals.try_tactic";
   try
-   tactic status
+   apply_tactic tactic status
   with
    (Fail _) as e -> 
     warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
-    id_tac status
+    apply_tactic id_tac status
+ in
+  mk_tactic (try_tactic ~tactic)
 ;;
 
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
-
-let rec solve_tactics ~(tactics: (string * tactic) list) status =
+let solve_tactics ~tactics =
+ let rec solve_tactics ~(tactics: (string * tactic) list) status =
   warn "in Tacticals.solve_tactics";
   match tactics with
   | (descr, currenttactic)::moretactics ->
       warn ("Tacticals.solve_tactics is trying " ^ descr);
       (try
-        let (proof, goallist) = currenttactic status in
+        let (proof, goallist) = apply_tactic currenttactic status in
          match goallist with 
-            [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!");
-(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *)
-(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
+            [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ 
+                  " solved the goal!!!");
+(* questo significa che non ci sono piu' goal, o che current_tactic non ne 
+   ha aperti di nuovi? (la 2a!) ##### 
+   nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
                   (proof, goallist)
           | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
                  solve_tactics ~tactics:(moretactics) status
        with
         (Fail _) as e ->
-         warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e);
+         warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ 
+         Printexc.to_string e);
          solve_tactics ~tactics status
       )
   | [] -> raise (Fail "solve_tactics cannot solve the goal");
-          id_tac status
+          apply_tactic id_tac status
+ in
+  mk_tactic (solve_tactics ~tactics)
 ;;
 
 
index daf461c5ba78ade83739de5cb180c79fccf9cc85..0566564dc276c863954bf4c43facd662ad5f7223 100644 (file)
@@ -56,6 +56,8 @@ let search_theorems_in_context status =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
+  let module PET = ProofEngineTypes in 
+  let module PT = PrimitiveTactics in 
   prerr_endline "Entro in search_context";
   let _,metasenv,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -64,9 +66,9 @@ let search_theorems_in_context status =
     | hd::tl ->
        let res =
          try 
-            Some (PrimitiveTactics.apply_tac status ~term:(C.Rel n)
+            Some (PET.apply_tactic (PT.apply_tac ~term:(C.Rel n)) status 
          with 
-           ProofEngineTypes.Fail _ -> None in
+           PET.Fail _ -> None in
        (match res with
          Some res -> res::(find (n+1) tl)
        | None -> find (n+1) tl)
@@ -147,17 +149,23 @@ prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
     | None -> proof
 ;;
 
-let auto_tac mqi_handle (proof,goal) =
+let auto_tac mqi_handle =
+ let module PET = ProofEngineTypes in
+ let auto_tac mqi_handle (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
     let proof = auto_tac_aux mqi_handle depth proof goal in
-prerr_endline "AUTO_TAC HA FINITO";
-    (proof,[])
+    prerr_endline "AUTO_TAC HA FINITO";
+     (proof,[])
   with 
   | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
   | NotApplicableTheorem -> 
       prerr_endline("No applicable theorem");
-      raise (ProofEngineTypes.Fail "No Applicable theorem");;
+      raise (ProofEngineTypes.Fail "No Applicable theorem")
+ in
+  PET.mk_tactic (auto_tac mqi_handle)
+;;
+
 *)
 
 (**** ESPERIMENTO ************************)
@@ -211,7 +219,8 @@ let rec auto_new mqi_handle = function
 ;;
 
 
-let auto_tac mqi_handle (proof,goal) =
+let auto_tac mqi_handle =
+ let auto_tac mqi_handle (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
     let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
@@ -220,17 +229,23 @@ prerr_endline "AUTO_TAC HA FINITO";
   with 
   | NoOtherChoices ->
       prerr_endline("Auto failed");
-      raise (ProofEngineTypes.Fail "No Applicable theorem");;
+      raise (ProofEngineTypes.Fail "No Applicable theorem")
+ in
+  ProofEngineTypes.mk_tactic (auto_tac mqi_handle)
+;;
 
 (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
 chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
 funzione di callback che restituisce la (sola) hyp da applicare *)
 
-let assumption_tac status =
+let assumption_tac =
+ let module PET = ProofEngineTypes in
+ let assumption_tac status =
   let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
+  let module PT = PrimitiveTactics in
    let _,metasenv,_,_ = proof in
     let _,context,ty = CicUtil.lookup_meta goal metasenv in
      let rec find n = function 
@@ -245,8 +260,10 @@ let assumption_tac status =
                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
            | _ -> find (n+1) tl
          )
-      | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
-     in PrimitiveTactics.apply_tac status ~term:(C.Rel (find 1 context))
+      | [] -> raise (PET.Fail "Assumption: No such assumption")
+     in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status
+ in
+  PET.mk_tactic assumption_tac
 ;;
 
 (* ANCORA DA DEBUGGARE *)
@@ -257,42 +274,46 @@ exception AllSelectedTermsMustBeConvertible;;
 e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
 contesto e si lifta di tot... COSA SIGNIFICA TUTTO CIO'?????? *)
 
-let generalize_tac
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name)
- terms status
-=
-  let (proof, goal) = status in
-  let module C = Cic in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-   let _,context,ty = CicUtil.lookup_meta goal metasenv in
-    let typ =
-     match terms with
-        [] -> assert false
-      | he::tl ->
-         (* We need to check that all the convertibility of all the terms *)
-         List.iter
-          (function t ->
-            if not (CicReduction.are_convertible context he t) then 
-             raise AllSelectedTermsMustBeConvertible
-          ) tl ;
-         (CicTypeChecker.type_of_aux' metasenv context he)
-    in
-     T.thens 
-      ~start:
-        (P.cut_tac 
-         (C.Prod(
-           (mk_fresh_name_callback metasenv context C.Anonymous typ), 
-           typ,
-           (ProofEngineReduction.replace_lifting_csc 1
-             ~equality:(==) 
-             ~what:terms
-             ~with_what:(List.map (function _ -> C.Rel 1) terms)
-             ~where:ty)
-         )))
-      ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
-      status
+let generalize_tac 
+ ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name) terms
+ =
+  let module PET = ProofEngineTypes in
+  let generalize_tac mk_fresh_name_callback terms status =
+   let (proof, goal) = status in
+   let module C = Cic in
+   let module P = PrimitiveTactics in
+   let module T = Tacticals in
+    let _,metasenv,_,_ = proof in
+    let _,context,ty = CicUtil.lookup_meta goal metasenv in
+     let typ =
+      match terms with
+         [] -> assert false
+       | he::tl ->
+          (* We need to check that all the convertibility of all the terms *)
+          List.iter
+           (function t ->
+             if not (CicReduction.are_convertible context he t) then 
+              raise AllSelectedTermsMustBeConvertible
+           ) tl ;
+          (CicTypeChecker.type_of_aux' metasenv context he)
+     in
+      PET.apply_tactic 
+      (T.thens 
+       ~start:
+         (P.cut_tac 
+          (C.Prod(
+            (mk_fresh_name_callback metasenv context C.Anonymous ~typ:typ), 
+            typ,
+            (ProofEngineReduction.replace_lifting_csc 1
+              ~equality:(==) 
+              ~what:terms
+              ~with_what:(List.map (function _ -> C.Rel 1) terms)
+              ~where:ty)
+          )))
+       ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac])
+       status
+ in
+  PET.mk_tactic (generalize_tac mk_fresh_name_callback terms)
 ;;
 
 
index c27e542ff1cbbe49513d7bb13532354b46c68223..a4d471e3b29011a859a6ad561b5004c2e5978467 100644 (file)
@@ -32,7 +32,5 @@ val generalize_tac:
  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
   ProofEngineTypes.tactic
 
-val auto_tac : 
- MQIConn.handle -> ProofEngineTypes.status ->
-   ProofEngineTypes.proof * ProofEngineTypes.goal list
+val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic