diff options
| -rw-r--r-- | dev/myinclude | 1 | ||||
| -rw-r--r-- | lia.cache | bin | 23 -> 0 bytes | |||
| -rw-r--r-- | parsing/g_obligations.ml4 | 135 | ||||
| -rw-r--r-- | tactics/nbtermdn.ml | 131 | ||||
| -rw-r--r-- | tactics/termdn.ml | 136 | ||||
| -rw-r--r-- | toplevel/g_obligations.ml4 | 2 |
6 files changed, 1 insertions, 404 deletions
diff --git a/dev/myinclude b/dev/myinclude deleted file mode 100644 index 48de3647a..000000000 --- a/dev/myinclude +++ /dev/null @@ -1 +0,0 @@ -#use "include";; diff --git a/lia.cache b/lia.cache Binary files differdeleted file mode 100644 index b878cf355..000000000 --- a/lia.cache +++ /dev/null diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 deleted file mode 100644 index 061f7ba5d..000000000 --- a/parsing/g_obligations.ml4 +++ /dev/null @@ -1,135 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "grammar/grammar.cma" i*) - -(* - Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) - - -open Libnames -open Constrexpr -open Constrexpr_ops - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac.<foo> - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -open Pcoq - -let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg None "withtac" - -let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac) - -GEXTEND Gram - GLOBAL: withtac; - - withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] - ] ]; - - END - -open Obligations - -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater) - -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] -END - -VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] -END - -VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] -END - -VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] -END - -VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - set_default_tactic - (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (Tacintern.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY -| [ "Show" "Obligation" "Tactic" ] -> [ - msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] -END - -VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ msg_info (show_term None) ] -END - -open Pp - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac - in - (* should not happen *) - let dummy _ _ _ expr = assert false in - Pptactic.declare_extra_genarg_pprule wit_withtac printer dummy dummy diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml deleted file mode 100644 index b07aff99b..000000000 --- a/tactics/nbtermdn.ml +++ /dev/null @@ -1,131 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Term -open Pattern -open Globnames - -(* Named, bounded-depth, term-discrimination nets. - Implementation: - Term-patterns are stored in discrimination-nets, which are - themselves stored in a hash-table, indexed by the first label. - They are also stored by name in a table on-the-side, so that we can - override them if needed. *) - -(* The former comments are from Chet. - See the module dn.ml for further explanations. - Eduardo (5/8/97) *) -module Make = - functor (Y:Map.OrderedType) -> -struct - module X = struct - type t = constr_pattern*int - let compare = Pervasives.compare - end - - module Term_dn = Termdn.Make(Y) - open Term_dn - module Z = struct - type t = Term_dn.term_label - let compare x y = - let make_name n = - match n with - | GRLabel(ConstRef con) -> - GRLabel(ConstRef(constant_of_kn(canonical_con con))) - | GRLabel(IndRef (kn,i)) -> - GRLabel(IndRef(mind_of_kn(canonical_mind kn),i)) - | GRLabel(ConstructRef ((kn,i),j ))-> - GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j)) - | k -> k - in - Pervasives.compare (make_name x) (make_name y) - end - - module Dn = Dn.Make(X)(Z)(Y) - module Bounded_net = Btermdn.Make(Y) - - -type 'na t = { - mutable table : ('na,constr_pattern * Y.t) Gmap.t; - mutable patterns : (Term_dn.term_label option,Bounded_net.t) Gmap.t } - - -type 'na frozen_t = - ('na,constr_pattern * Y.t) Gmap.t - * (Term_dn.term_label option, Bounded_net.t) Gmap.t - -let create () = - { table = Gmap.empty; - patterns = Gmap.empty } - -let get_dn dnm hkey = - try Gmap.find hkey dnm with Not_found -> Bounded_net.create () - -let add dn (na,(pat,valu)) = - let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in - dn.table <- Gmap.add na (pat,valu) dn.table; - let dnm = dn.patterns in - dn.patterns <- Gmap.add hkey (Bounded_net.add None (get_dn dnm hkey) (pat,valu)) dnm - -let rmv dn na = - let (pat,valu) = Gmap.find na dn.table in - let hkey = Option.map fst (Term_dn.constr_pat_discr pat) in - dn.table <- Gmap.remove na dn.table; - let dnm = dn.patterns in - dn.patterns <- Gmap.add hkey (Bounded_net.rmv None (get_dn dnm hkey) (pat,valu)) dnm - -let in_dn dn na = Gmap.mem na dn.table - -let remap ndn na (pat,valu) = - rmv ndn na; - add ndn (na,(pat,valu)) - -let decomp = - let rec decrec acc c = match kind_of_term c with - | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Cast (c1,_,_) -> decrec acc c1 - | _ -> (c,acc) - in - decrec [] - - let constr_val_discr t = - let c, l = decomp t in - match kind_of_term c with - | Ind (ind_sp,_) -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l) - | Construct (cstr_sp,_) -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l) - | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l) - | Const _ -> Dn.Everything - | _ -> Dn.Nothing - -let lookup dn valu = - let hkey = - match (constr_val_discr valu) with - | Dn.Label(l,_) -> Some l - | _ -> None - in - try Bounded_net.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> [] - -let app f dn = Gmap.iter f dn.table - -let dnet_depth = Btermdn.dnet_depth - -let freeze dn = (dn.table, dn.patterns) - -let unfreeze (fnm,fdnm) dn = - dn.table <- fnm; - dn.patterns <- fdnm - -let empty dn = - dn.table <- Gmap.empty; - dn.patterns <- Gmap.empty - -let to2lists dn = - (Gmap.to_list dn.table, Gmap.to_list dn.patterns) -end diff --git a/tactics/termdn.ml b/tactics/termdn.ml deleted file mode 100644 index 1c4c4b648..000000000 --- a/tactics/termdn.ml +++ /dev/null @@ -1,136 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Term -open Pattern -open Patternops -open Globnames - -(* Discrimination nets of terms. - See the module dn.ml for further explanations. - Eduardo (5/8/97) *) -module Make = - functor (Z : Map.OrderedType) -> -struct - - module X = struct - type t = constr_pattern - let compare = Pervasives.compare (** FIXME *) - end - - type term_label = - | GRLabel of global_reference - | ProdLabel - | LambdaLabel - | SortLabel - - module Y = struct - type t = term_label - let compare x y = - let make_name n = - match n with - | GRLabel(ConstRef con) -> - GRLabel(ConstRef(constant_of_kn(canonical_con con))) - | GRLabel(IndRef (kn,i)) -> - GRLabel(IndRef(mind_of_kn(canonical_mind kn),i)) - | GRLabel(ConstructRef ((kn,i),j ))-> - GRLabel(ConstructRef((mind_of_kn(canonical_mind kn),i),j)) - | k -> k - in - Pervasives.compare (make_name x) (make_name y) - end - - - module Dn = Dn.Make(X)(Y)(Z) - - type t = Dn.t - - type 'a lookup_res = 'a Dn.lookup_res - -(*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*) - -let decomp = - let rec decrec acc c = match kind_of_term c with - | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Cast (c1,_,_) -> decrec acc c1 - | Proj (p, c) -> decrec (c :: acc) (mkConst p) - | _ -> (c,acc) - in - decrec [] - -let decomp_pat = - let rec decrec acc = function - | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | c -> (c,acc) - in - decrec [] - -let constr_pat_discr t = - if not (occur_meta_pattern t) then - None - else - match decomp_pat t with - | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args) - | _ -> None - -let constr_pat_discr_st (idpred,cpred) t = - match decomp_pat t with - | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) -> - Some(GRLabel ref,args) - | PVar v, args when not (Id.Pred.mem v idpred) -> - Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> - Some (GRLabel ref, args) - | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) - | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) - | PSort s, [] -> Some (SortLabel, []) - | _ -> None - -open Dn - -let constr_val_discr t = - let c, l = decomp t in - match kind_of_term c with - | Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l) - | Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id -> Label(GRLabel (VarRef id),l) - | Const _ -> Everything - | Proj _ -> Everything - | _ -> Nothing - -let constr_val_discr_st (idpred,cpred) t = - let c, l = decomp t in - match kind_of_term c with - | Const (c,_) -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) - | Ind (ind_sp,_) -> Label(GRLabel (IndRef ind_sp),l) - | Construct (cstr_sp,_) -> Label(GRLabel (ConstructRef cstr_sp),l) - | Proj (p,c) -> if Cpred.mem p cpred then Everything else Label(GRLabel (ConstRef p),c::l) - | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) - | Prod (n, d, c) -> Label(ProdLabel, [d; c]) - | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) - | Sort _ -> Label (SortLabel, []) - | Evar _ -> Everything - | _ -> Nothing - -let create = Dn.create - -let add dn st = Dn.add dn (constr_pat_discr_st st) - -let rmv dn st = Dn.rmv dn (constr_pat_discr_st st) - -let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t - -let app f dn = Dn.app f dn - -end diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 2354aa332..061f7ba5d 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -54,7 +54,7 @@ GEXTEND Gram open Obligations -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater) +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",GuaranteesOpacity,[],false), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> |