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
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
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
;;
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
(* 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 ();
(* *)
(******************************************************************************)
-(*
+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 -> ()
* 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 *)
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) ->
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 ->
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 =
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
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 *)
(* 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 ;
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
+;;
(* 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) *)
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,_) ->
("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
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
("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
| _ ->
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
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
| 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 _
(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
| 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")
| 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 ()))
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
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 *)
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 ->
*)
;;
+(* 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
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
;;
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 *)
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
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
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 \
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
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 \
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
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 \
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
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) -> (
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)))
)
| _ -> 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)
;;
(* 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
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
let _,context',gty' =
CicUtil.lookup_meta goal' metasenv'
in
- T.then_
+ ProofEngineTypes.apply_tactic
+ (T.then_
~start:
(P.change_tac
~what:gty'
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)
;;
-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
;;
*)
-
-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)
;;
;;
*)
-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
| 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)
;;
* 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
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 [
~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)
;;
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
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)
;;
*)
open Fourier
+open ProofEngineTypes
let debug x = print_string ("____ "^x) ; flush stdout;;
(* 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" );
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))
;;
(* 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))
;;
(* 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
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) ->
[(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
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
(* 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
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 ) *)
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");
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;
(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
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
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:=*)
|_-> 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
* 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
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) ;;
* 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
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
(* 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 *)
(*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)
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)
(** 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
--- /dev/null
+(* 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
* http://cs.unibo.it/helm/.
*)
+open ProofEngineTypes
+
(*
let reduction_tac ~reduction (proof,goal) =
let curi,metasenv,pbo,pty = proof in
(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)
;;
@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
(**
@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 =
| (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
let proof',goal' = aux count context status in
assert (goal = goal') ;
proof',[goal']
+ in
+ ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
(** THE TACTIC! *)
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";
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'' ;
] ;
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
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 ...",
] ;
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
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
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
+
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;
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) );
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 *)
(* 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
(**
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
| _ -> 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? *)
(* 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, [])
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
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)
;;
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
| 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)
| 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 ************************)
;;
-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
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
(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 *)
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)
;;
?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
projects / helm.git / commitdiff