Permalink
Browse files

Cleanup before merge with the trunk

  • Loading branch information...
mattam82 committed May 6, 2014
1 parent 8fba837 commit 0857007106234d46e1b30170f36635ad631653c6
Showing with 1 addition and 404 deletions.
  1. +0 −1 dev/myinclude
  2. BIN lia.cache
  3. +0 −135 parsing/g_obligations.ml4
  4. +0 −131 tactics/nbtermdn.ml
  5. +0 −136 tactics/termdn.ml
  6. +1 −1 toplevel/g_obligations.ml4
View
@@ -1 +0,0 @@
-#use "include";;
View
BIN lia.cache
Binary file not shown.
View
@@ -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
View
@@ -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
Oops, something went wrong.

0 comments on commit 0857007

Please sign in to comment.