(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
let names = match ident with None -> [] | Some id -> [id] in
Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
| GrafiteAst.DecideEquality _ -> Tactics.decide_equality
- | GrafiteAst.Decompose (_,term) -> Tactics.decompose term
+ | GrafiteAst.Decompose (_, types, what, names) ->
+ let to_type = function
+ | GrafiteAst.Type (uri, typeno) -> uri, typeno
+ | GrafiteAst.Ident _ -> assert false
+ in
+ let user_types = List.rev_map to_type types in
+ let dbd = MatitaDb.instance () in
+ let mk_fresh_name_callback = namer_of names in
+ Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
| GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
status, GrafiteAst.Cut (loc, ident, cic)
| GrafiteAst.DecideEquality loc ->
status, GrafiteAst.DecideEquality loc
- | GrafiteAst.Decompose (loc,term) ->
- let status,term = disambiguate_term status term in
- status, GrafiteAst.Decompose(loc,term)
+ | GrafiteAst.Decompose (loc, types, what, names) ->
+ let disambiguate (status, types) = function
+ | GrafiteAst.Type _ -> assert false
+ | GrafiteAst.Ident id ->
+ match disambiguate_term status (CicNotationPt.Ident (id, None)) with
+ | status, Cic.MutInd (uri, tyno, _) ->
+ status, (GrafiteAst.Type (uri, tyno) :: types)
+ | _ ->
+ raise Disambiguate.NoWellTypedInterpretation
+ in
+ let status, types = List.fold_left disambiguate (status, []) types in
+ status, GrafiteAst.Decompose(loc, types, what, names)
| GrafiteAst.Discriminate (loc,term) ->
let status,term = disambiguate_term status term in
status, GrafiteAst.Discriminate(loc,term)
theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)).
intros. auto.
qed.
+
(*
theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
-intros 1. elim x.
-clear x. auto.
-clear H. fwd H1 [H]. decompose H.
+intros 1. elim x; clear H. (* clear x *)
+auto.
+fwd H1 [H]. decompose H.
*)
-
type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+type ('term, 'ident) type_spec =
+ | Ident of 'ident
+ | Type of UriManager.uri * int
+
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Contradiction of loc
| Cut of loc * 'ident option * 'term
| DecideEquality of loc
- | Decompose of loc * 'term
+ | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list
"cut " ^ pp_term_ast term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| DecideEquality _ -> "decide equality"
- | Decompose (_, term) ->
- sprintf "decompose %s" (pp_term_ast term)
+ | Decompose (_, [], what, names) ->
+ sprintf "decompose %s%s" what (pp_intros_specs (None, names))
+ | Decompose (_, types, what, names) ->
+ let to_ident = function
+ | Ident id -> id
+ | Type _ -> assert false
+ in
+ let types = List.rev_map to_ident types in
+ sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names))
| Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ pp_term_ast term ^
GrafiteAst.Cut (loc, ident, t)
| IDENT "decide"; IDENT "equality" ->
GrafiteAst.DecideEquality loc
- | IDENT "decompose"; where = tactic_term ->
- GrafiteAst.Decompose (loc, where)
+ | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
+ OPT "names"; num = OPT [num = int -> num];
+ idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ let types = match types with None -> [] | Some types -> types in
+ let to_spec id = GrafiteAst.Ident id in
+ GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "discriminate"; t = tactic_term ->
GrafiteAst.Discriminate (loc, t)
| IDENT "elim"; what = tactic_term;
type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
+type ('term, 'ident) type_spec =
+ | Ident of 'ident
+ | Type of UriManager.uri * int
+
type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
| Contradiction of loc
| Cut of loc * 'ident option * 'term
| DecideEquality of loc
- | Decompose of loc * 'term
+ | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list
"cut " ^ pp_term_ast term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| DecideEquality _ -> "decide equality"
- | Decompose (_, term) ->
- sprintf "decompose %s" (pp_term_ast term)
+ | Decompose (_, [], what, names) ->
+ sprintf "decompose %s%s" what (pp_intros_specs (None, names))
+ | Decompose (_, types, what, names) ->
+ let to_ident = function
+ | Ident id -> id
+ | Type _ -> assert false
+ in
+ let types = List.rev_map to_ident types in
+ sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names))
| Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ pp_term_ast term ^
* http://cs.unibo.it/helm/.
*)
-(** DEBUGGING *)
-
- (** perform debugging output? *)
-let debug = false
-let debug_print = fun _ -> ()
-
- (** debugging print *)
-let warn s =
- if debug then
- debug_print ("DECOMPOSE: " ^ s)
-
-
+module C = Cic
+module P = PrimitiveTactics
+module T = Tacticals
+module S = ProofEngineStructuralRules
+module F = FreshNamesGenerator
+module E = ProofEngineTypes
+module H = ProofEngineHelpers
+module Q = MetadataQuery
(*
let induction_tac ~term status =
;;
*)
-let elim_type_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+(* unexported tactics *******************************************************)
+
+let get_name context index =
+ try match List.nth context (pred index) with
+ | Some (Cic.Name name, _) -> Some name
+ | _ -> None
+ with Invalid_argument "List.nth" -> None
+
+let rec scan_tac ~old_context_length ~index ~tactic =
+ let scan_tac status =
+ let (proof, goal) = status in
+ let _, metasenv, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let context_length = List.length context in
+ let rec aux index =
+ match get_name context index with
+ | _ when index <= 0 -> (proof, [goal])
+ | None -> aux (pred index)
+ | Some what ->
+ let tac = T.then_ ~start:(tactic ~what)
+ ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic)
+ in
+ try E.apply_tactic tac status
+ with E.Fail _ -> aux (pred index)
+ in aux (index + context_length - old_context_length - 1)
+ in
+ E.mk_tactic scan_tac
+
+let rec check_inductive_types types = function
+ | C.MutInd (uri, typeno, _) -> List.mem (uri, typeno) types
+ | C.Appl (hd :: tl) -> check_inductive_types types hd
+ | _ -> false
+
+let elim_clear_tac ~mk_fresh_name_callback ~types ~what =
+ let elim_clear_tac status =
+ let (proof, goal) = status in
+ let _, metasenv, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let index, ty = H.lookup_type metasenv context what in
+ if check_inductive_types types ty then
+ let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+ ~continuation:(S.clear what)
+ in
+ E.apply_tactic tac status
+ else raise (E.Fail "unexported elim_clear: not an eliminable type")
+ in
+ E.mk_tactic elim_clear_tac
+
+(* elim type ****************************************************************)
+
+let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
?depth ?using what =
- let elim_type_tac 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 what)
- ~continuations:[ P.elim_intros_simpl_tac ?depth ?using ~mk_fresh_name_callback (C.Rel 1) ; T.id_tac ])
- status
- in
- ProofEngineTypes.mk_tactic elim_type_tac
-;;
+ let elim what = P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what in
+ let elim_type_tac status =
+ let tac = T.thens ~start: (P.cut_tac what)
+ ~continuations:[elim (C.Rel 1); T.id_tac]
+ in
+ E.apply_tactic tac status
+ in
+ E.mk_tactic elim_type_tac
+(* decompose ****************************************************************)
-(* Decompose related stuff *)
+(* robaglia --------------------------------------------------------------- *)
-exception InteractiveUserUriChoiceNotRegistered
+ (** perform debugging output? *)
+let debug = false
+let debug_print = fun _ -> ()
-let interactive_user_uri_choice =
- (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) :
- (selection_mode:[`SINGLE | `EXTENDED] ->
- ?ok:string ->
- ?enable_button_for_non_vars:bool ->
- title:string -> msg:string -> string list -> string list) ref)
-;;
+ (** debugging print *)
+let warn s =
+ if debug then
+ debug_print ("DECOMPOSE: " ^ s)
-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
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let module S = ProofEngineStructuralRules in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let old_context_len = List.length context in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let rec make_list termty =
- (* N.B.: altamente inefficente? *)
- let rec search_inductive_types urilist termty =
- (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
- match termty with
- (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) ->
- (uri,typeno,exp_named_subst)::urilist
- | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) ->
- (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist)
- | _ -> urilist
- (* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *)
- in
- let rec purge_duplicates urilist =
- let rec aux triple urilist =
- match urilist with
- [] -> []
- | hd::tl ->
- if (hd = triple)
- then aux triple tl
- else hd::(aux triple tl)
- in
- match urilist with
- [] -> []
- | hd::tl -> hd::(purge_duplicates (aux hd tl))
- in
- purge_duplicates (search_inductive_types [] termty)
+(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
+let search_inductive_types ty =
+ let rec aux types = function
+ | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) ->
+ (uri, typeno) :: types
+ | C.Appl applist -> List.fold_left aux types applist
+ | _ -> types
+ in
+ aux [] ty
+(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *)
+
+(* roba seria ------------------------------------------------------------- *)
+
+let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
+ ?(user_types=[]) ~dbd what =
+ let decompose_tac status =
+ let (proof, goal) = status in
+ let _, metasenv,_,_ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let types = List.rev_append user_types (Q.decomposables dbd) in
+ let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in
+ let old_context_length = List.length context in
+ let tac = T.then_ ~start:(tactic ~what)
+ ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
in
+ E.apply_tactic tac status
+ in
+ E.mk_tactic decompose_tac
+
+(*
+module R = CicReduction
- let urilist =
- (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *)
- (* N.B.: due to a bug in uris_choice_callback exp_named_subst are not significant (they all are []) *)
- uris_choice_callback (make_list termty) in
-
- let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
+ let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
let (proof, goal) = status in
warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim));
if nr_of_hyp_still_to_elim <> 0 then
in
elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status
- in
- ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term)
-;;
-
-
+*)
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
-(* The default callback always decomposes the term as much as possible *)
val decompose_tac:
- ?uris_choice_callback:
- ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
- (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
- Cic.term ->
- ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?user_types:((UriManager.uri * int) list) ->
+ dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic
* http://cs.unibo.it/helm/.
*)
-(*
+
module PEH = ProofEngineHelpers
-*)
module U = CicUniv
module TC = CicTypeChecker
module PET = ProofEngineTypes
module PESR = ProofEngineStructuralRules
let fail_msg0 = "unexported clearbody: invalid argument"
-let fail_msg1 = "fwd: argument is not premise in the current goal"
let fail_msg2 = "fwd: no applicable simplification"
let error msg = raise (PET.Fail msg)
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
- let conclusion = Cic.Appl (what :: List.rev metas) in
+ let conclusion =
+ match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
+ in
let tac = T.thens ~start:(letin_tac conclusion)
~continuations:[clearbody ~index:1]
in
(* fwd **********************************************************************)
let fwd_simpl_tac
- ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ~dbd hyp
- =
- let find_type metasenv context =
- let rec aux p = function
- | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
- p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph)
- | _ :: tail -> aux (succ p) tail
- | [] -> error fail_msg1
- in
- aux 1 context
- in
+ ?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[])
+ ~dbd hyp =
let lapply_tac to_what lemma =
lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma
in
let (proof, goal) = status in
let _, metasenv, _, _ = proof in
let _, context, ty = CicUtil.lookup_meta goal metasenv in
- let index, major = find_type metasenv context in
+ let index, major = PEH.lookup_type metasenv context hyp in
match MetadataQuery.fwd_simpl ~dbd major with
| [] -> error fail_msg2
| uri :: _ ->
(Mysql.escape (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
let result = Mysql.exec dbd query in
- let lemmas = Mysql.map result ~f:(map inners) in
+ let lemmas = Mysql.map ~f:(map inners) result in
let ranked = List.fold_left rank [] lemmas in
let ordered = List.rev (List.fast_sort compare ranked) in
map_filter filter 0 ordered
+
+(* get_decomposables ********************************************************)
+
+let decomposables ~dbd =
+ let map row = match row.(0) with
+ | None -> None
+ | Some str ->
+ match CicUtil.term_of_uri (UriManager.uri_of_string str) with
+ | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno)
+ | _ ->
+ raise (UriManager.IllFormedUri str)
+ in
+ let select, from = "source", "decomposables" in
+ let query = Printf.sprintf "SELECT %s FROM %s" select from in
+ let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in
+ map_filter (fun _ x -> x) 0 decomposables
val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
+val decomposables: dbd:Mysql.dbd -> (UriManager.uri * int) list
let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
res,metasenv @ newmetasenv,arguments,lastmeta
+let lookup_type metasenv context hyp =
+ let rec aux p = function
+ | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
+ | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
+ p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+ | _ :: tail -> aux (succ p) tail
+ | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+ in
+ aux 1 context
val saturate_term:
int -> Cic.metasenv -> Cic.context -> Cic.term ->
Cic.term * Cic.metasenv * Cic.term list * int
+
+(* returns the index and the type of a premise in a context *)
+val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
+
Cic.term -> ProofEngineTypes.tactic
val decide_equality : ProofEngineTypes.tactic
val decompose :
- ?uris_choice_callback:((UriManager.uri * int *
- (UriManager.uri * Cic.term) list)
- list ->
- (UriManager.uri * int *
- (UriManager.uri * Cic.term) list)
- list) ->
- Cic.term -> ProofEngineTypes.tactic
+ ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?user_types:(UriManager.uri * int) list ->
+ dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic
val discriminate : term:Cic.term -> ProofEngineTypes.tactic
val elim_intros :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
projects / helm.git / commitdiff