[opentheory-users] Fwd: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory
Joe Hurd
joe at gilith.com
Mon Jan 10 18:58:02 UTC 2011
Hi Ramana,
This looks excellent - I will give it a go as soon as I get some time.
Cheers,
Joe
On Mon, Jan 10, 2011 at 9:35 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> My new implementation of the article reader for HOL4 (svn r8845) now
> successfully reads bool-1.0 (although I didn't check all the theorems
> were there - it looks reasonable, though).
>
> In the HOL repo, src/opentheory/selftest.sml is an example of how to
> use the reader, and src/opentheory/Opentheory.sig has some descriptive
> comments.
>
>
> ---------- Forwarded message ----------
> From: <xrchz at users.sourceforge.net>
> Date: Mon, Jan 10, 2011 at 5:32 PM
> Subject: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory
> To: hol-checkins at lists.sf.net
>
>
> Revision: 8845
> http://hol.svn.sourceforge.net/hol/?rev=8845&view=rev
> Author: xrchz
> Date: 2011-01-10 17:32:29 +0000 (Mon, 10 Jan 2011)
>
> Log Message:
> -----------
> Complete rewrite of Opentheory reader
>
> It now successfully reads the package bool-1.0 in the gilith repository,
> and that is the selftest (only runs if you have opentheory installed).
>
> The selftest file is also an example of the work you might need to do to
> read an opentheory article that defines constants that are already
> defined in HOL.
>
> When the article is only going to define new things, the work would
> likely be less, although some helper functions (TODO) in the Opentheory
> module would make it easier.
>
> Modified Paths:
> --------------
> HOL/src/opentheory/Opentheory.sig
> HOL/src/opentheory/Opentheory.sml
> HOL/src/opentheory/selftest.sml
>
> Modified: HOL/src/opentheory/Opentheory.sig
> ===================================================================
> --- HOL/src/opentheory/Opentheory.sig 2011-01-10 06:01:44 UTC (rev 8844)
> +++ HOL/src/opentheory/Opentheory.sig 2011-01-10 17:32:29 UTC (rev 8845)
> @@ -1,12 +1,51 @@
> signature Opentheory = sig
> - type thms = Thm.thm Net.net
> - type types = (string, Type.hol_type list -> Type.hol_type) Redblackmap.dict
> - type consts = (string, Type.hol_type -> Term.term) Redblackmap.dict
> - val empty_thms : thms
> - val empty_types : types
> - val empty_consts : consts
> - val thmsFromList : Thm.thm list -> thms
> - val typesFromList : (string * (Type.hol_type list ->
> Type.hol_type)) list -> types
> - val constsFromList : (string * (Type.hol_type -> Term.term)) list -> consts
> - val read_article : TextIO.instream ->
> {thms:thms,types:types,consts:consts} -> Thm.thm list
> +type term = Term.term type hol_type = Type.hol_type type thm = Thm.thm
> +type ('a,'b) dict = ('a,'b) Redblackmap.dict
> +
> +(* maps between OpenTheory names and HOL4 names: *)
> +type thy_tyop = {Thy:string,Tyop:string}
> +type thy_const = {Thy:string,Name:string}
> +type 'a to_ot = ('a,string) dict
> +type 'a from_ot= (string,'a) dict
> +val tyop_to_ot : unit -> thy_tyop to_ot
> +val tyop_from_ot : unit -> thy_tyop from_ot
> +val const_to_ot : unit -> thy_const to_ot
> +val const_from_ot: unit -> thy_const from_ot
> +
> +(* record of data an article reader must provide: *)
> +type reader = {
> + tyops : (string, {axiom:thm, args:hol_type list, rep:string, abs:string} ->
> + {rep_abs:thm, abs_rep:thm, rep:term, abs:term,
> tyop:thy_tyop})
> + dict,
> + consts : (string, term -> {const:thy_const, def:thm}) dict,
> + axioms : thm Net.net -> (term list * term) -> thm}
> +
> +(*
> +tyops are type operators the article will define, indexed by their OpenTheory
> +names. Each name is mapped to a function that does something equivalent to
> +defining the new type. Each function is provided the type axiom, a list of
> +arguments (type variables) for the type operator in the desired order, and the
> +OpenTheory names of the rep and abs constants. It must return the new type
> +operator, the rep and abs constants, and the type bijection theorems.
> +If axiom = |- P t then these are:
> + abs_rep = |- (!a. abs (rep a) = a)
> + rep_abs = |- (!r. P r = (rep(abs r) = r))
> +
> +consts are constants the article will define, indexed by their OpenTheory
> +names. Each name is mapped to a function that does something equivalent to
> +defining the new constant. Each function is provided the right hand side rhs of
> +the definition and must return the name of the constant and an equational
> +theorem |- const = rhs.
> +
> +axioms are theorems that the article depends on about possibly both input
> +and output tyops and constants. They are represented by a function that takes
> +the collection of theorems the article has already proved, represented by a
> +conclusion-indexed net, and a pair (h,c) representing the desired axiom, and
> +must return a theorem h |- c.
> +*)
> +
> +val raw_read_article : {tyop_from_ot:thy_tyop from_ot,
> + const_from_ot:thy_const from_ot}
> + -> TextIO.instream -> reader -> thm list
> +val read_article : string -> reader -> thm list
> end
>
> Modified: HOL/src/opentheory/Opentheory.sml
> ===================================================================
> --- HOL/src/opentheory/Opentheory.sml 2011-01-10 06:01:44 UTC (rev 8844)
> +++ HOL/src/opentheory/Opentheory.sml 2011-01-10 17:32:29 UTC (rev 8845)
> @@ -1,221 +1,162 @@
> structure Opentheory :> Opentheory = struct
>
> -val ERR = Feedback.mk_HOL_ERR "Opentheory"
> +open boolSyntax HolKernel Parse
>
> +local open Drule Conv in
> + fun DEDUCT_ANTISYM th1 th2 =
> + IMP_ANTISYM_RULE
> + (DISCH (concl th2) th1)
> + (DISCH (concl th1) th2)
> + fun absThm (v,tu) = let
> + val (t,u) = dest_eq(concl tu)
> + val vt = mk_abs(v,t)
> + val vu = mk_abs(v,u)
> + val vtvu = mk_eq(vt,vu)
> + val x = FUN_EQ_CONV vtvu
> + val x = CONV_RULE (RAND_CONV (QUANT_CONV (LAND_CONV BETA_CONV))) x
> + val x = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) x
> + in EQ_MP (SYM x) (GEN v tu) end
> +end
> +
> +val ERR = mk_HOL_ERR "Opentheory"
> +
> structure Map = Redblackmap
> -type thms = Thm.thm Net.net
> -type types = (string, Type.hol_type list -> Type.hol_type) Map.dict
> -type consts = (string, Type.hol_type -> Term.term) Map.dict
> +type ('a,'b) dict = ('a,'b) Map.dict
>
> -val empty_thms = Net.empty
> -val empty_types = Map.mkDict String.compare
> -val empty_consts = Map.mkDict String.compare
> -val thmsFromList = List.foldl (fn (th,n) => Net.insert(Thm.concl
> th,th) n) empty_thms
> -val typesFromList = Map.fromList String.compare
> -val constsFromList = Map.fromList String.compare
> +type thy_tyop = {Thy:string,Tyop:string}
> +type thy_const = {Thy:string,Name:string}
> +type 'a to_ot = ('a,string) dict
> +type 'a from_ot= (string,'a) dict
> +fun lex_cmp c (f1,f2) (x1,x2) =
> + case c(f1 x1,f1 x2) of EQUAL => c(f2 x1,f2 x2) | z => z
> +val thy_tyop_cmp = lex_cmp String.compare (#Tyop,#Thy)
> +val thy_const_cmp = lex_cmp String.compare (#Name,#Thy)
> +val the_tyop_to_ot = ref (Map.mkDict thy_tyop_cmp)
> +val the_tyop_from_ot = ref (Map.mkDict String.compare)
> +val the_const_to_ot = ref (Map.mkDict thy_const_cmp)
> +val the_const_from_ot= ref (Map.mkDict String.compare)
> +fun tyop_to_ot() = !the_tyop_to_ot
> +fun tyop_from_ot() = !the_tyop_from_ot
> +fun const_to_ot() = !the_const_to_ot
> +fun const_from_ot()= !the_const_from_ot
>
> datatype object
> = ONum of int
> | OName of string
> | OList of object list
> -| OTypeOp of string
> -| OType of Type.hol_type
> -| OConst of string
> -| OVar of Term.term
> -| OTerm of Term.term
> -| OThm of Thm.thm
> +| OTypeOp of thy_tyop
> +| OType of hol_type
> +| OConst of thy_const
> +| OVar of term
> +| OTerm of term
> +| OThm of thm
>
> -datatype command
> -= Num of int
> -| Name of string
> -| AbsTerm
> -| AbsThm
> -| AppTerm
> -| AppThm
> -| Assume
> -| Axiom
> -| BetaConv
> -| Cons
> -| Const
> -| ConstTerm
> -| DeductAntisym
> -| Def
> -| DefineConst
> -| DefineTypeOp
> -| EqMp
> -| Nil
> -| OpType
> -| Pop
> -| Ref
> -| Refl
> -| Remove
> -| Subst
> -| Thm
> -| TypeOp
> -| Var
> -| VarTerm
> -| VarType
> +type reader =
> + {tyops : (string, {axiom:thm, args:hol_type list, rep:string,
> abs:string} ->
> + {rep_abs:thm, abs_rep:thm, rep:term, abs:term,
> tyop:thy_tyop})
> + dict,
> + consts : (string, term -> {const:thy_const, def:thm}) dict,
> + axioms : thm Net.net -> (term list * term) -> thm}
>
> -fun st_ (st,{stack,dict,thms}) = {stack=st,dict=dict,thms=thms}
> -fun push (ob,state) = st_ (ob::(#stack state),state)
> -
> -fun find_thm thms (h,c) = let
> - val candidates = Net.index c thms
> - fun equal thm = let
> - val c' = Thm.concl thm
> - val thm' = Drule.PART_MATCH Lib.I thm (#2(boolSyntax.strip_forall c))
> - in Lib.set_eq h (Thm.hyp thm') end handle Feedback.HOL_ERR _ => false
> - val SOME th = List.find equal candidates
> -in th end
> -
> -fun find_const consts (n,t) = Map.find(consts,n) t
> -handle Map.NotFound => Term.mk_const(n,t)
> -handle Feedback.HOL_ERR _ => raise ERR "find_const" ("need "^n^" of
> type "^(Parse.type_to_string t))
> -
> -local open Thm Drule in
> -fun DEDUCT_ANTISYM th1 th2 =
> - IMP_ANTISYM_RULE
> - (DISCH (concl th1) th2)
> - (DISCH (concl th2) th1)
> +fun st_(st,{stack,dict,thms}) = {stack=st,dict=dict,thms=thms}
> +fun push (ob,st) = st_(ob::(#stack st),st)
> +local open Substring in
> + val trimlr = fn s => string(trimr 1 (triml 1 (full s)))
> + val trimr = fn s => string(trimr 1 (full s))
> end
>
> -val unOTermls = List.map (fn OTerm t => t)
> -val unOTypels = List.map (fn OType t => t)
> -val unONamels = List.map (fn OName n => n)
> -
> -fun find_type types (t,ls) = let
> - val ls = unOTypels ls
> -in
> - (Map.find(types,t)) ls
> - handle Map.NotFound => let
> - val s = Parse.type_to_string(Type.mk_type(t,ls))
> - handle Feedback.HOL_ERR _ =>
> - (* PolyML.makestring (t, (Map.listItems types)) *)
> - ("TyOp = "^t^", Args = "^(String.concatWith ", " (List.map
> Parse.type_to_string ls)))
> - in raise ERR "find_type" ("need "^s) end
> -end
> -
> -exception Comment
> -
> -fun
> - parse_line "absTerm" = AbsTerm
> -| parse_line "absThm" = AbsThm
> -| parse_line "appTerm" = AppTerm
> -| parse_line "appThm" = AppThm
> -| parse_line "assume" = Assume
> -| parse_line "axiom" = Axiom
> -| parse_line "betaConv" = BetaConv
> -| parse_line "cons" = Cons
> -| parse_line "const" = Const
> -| parse_line "constTerm" = ConstTerm
> -| parse_line "deductAntisym" = DeductAntisym
> -| parse_line "def" = Def
> -| parse_line "defineConst" = DefineConst
> -| parse_line "defineTypeOp" = DefineTypeOp
> -| parse_line "eqMp" = EqMp
> -| parse_line "nil" = Nil
> -| parse_line "opType" = OpType
> -| parse_line "pop" = Pop
> -| parse_line "ref" = Ref
> -| parse_line "refl" = Refl
> -| parse_line "remove" = Remove
> -| parse_line "subst" = Subst
> -| parse_line "thm" = Thm
> -| parse_line "typeOp" = TypeOp
> -| parse_line "var" = Var
> -| parse_line "varTerm" = VarTerm
> -| parse_line "varType" = VarType
> -| parse_line s = let
> - val c = String.sub(s,0)
> - in if c = #"\"" then Name (String.substring(s,1,String.size s -2)) else
> - if Char.isDigit c then Num (Option.valOf (Int.fromString s))
> - else raise Comment
> - end
> -
> -fun read_article file {types,consts,thms} = let
> - val find_asm = find_thm thms
> - val find_const = find_const consts
> - val find_type = find_type types
> - fun f (Num i) st = push(ONum i,st)
> - | f (Name s) st = push(OName s,st)
> - | f AbsTerm (st as {stack=OTerm b::OVar v::os,...}) =
> st_(OTerm(Term.mk_abs(v,b))::os,st)
> - | f AppTerm (st as {stack=OTerm x::OTerm f::os,...}) =
> st_(OTerm(Term.mk_comb(f,x))::os,st)
> - | f AppThm (st as {stack=OThm xy::OThm fg::os,...}) = let
> - val (f,g) = boolSyntax.dest_eq(Thm.concl fg)
> - val (x,y) = boolSyntax.dest_eq(Thm.concl xy)
> - val fxgx = Thm.AP_THM fg x
> - val gxgy = Thm.AP_TERM g xy
> - in st_(OThm(Thm.TRANS fxgx gxgy)::os,st) end
> - | f Assume (st as {stack=OTerm t::os,...}) =
> st_(OThm(Thm.ASSUME t)::os,st)
> - | f Axiom (st as {stack=OTerm t::OList ts::os,...}) =
> st_(OThm(find_asm(unOTermls ts,t))::os,st)
> - | f BetaConv (st as {stack=OTerm t::os,...}) =
> st_(OThm(Thm.BETA_CONV t)::os,st)
> - | f Cons (st as {stack=OList t::h::os,...}) =
> st_(OList(h::t)::os,st)
> - | f Const (st as {stack=OName n::os,...}) =
> st_(OConst n::os,st)
> - | f ConstTerm (st as {stack=OType t::OConst c::os,...}) =
> st_(OTerm(find_const (c,t))::os,st)
> - | f DeductAntisym (st as {stack=OThm t1::OThm t2::os,...}) =
> st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
> - | f Def {stack=ONum k::x::os,dict,thms} =
> {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
> - | f DefineConst (st as {stack=OTerm t::OName n::os,...}) = let
> - val t = boolSyntax.mk_eq(Term.mk_var(n,Term.type_of t),t)
> - val def = Definition.new_definition(n,t)
> - handle Feedback.HOL_ERR _ => raise ERR "read_article"
> ("DefineConst "^n^" by "^Parse.term_to_string t^" failed")
> - in st_(OThm def::OConst n::os,st) end
> - | f DefineTypeOp (st as {stack=OThm th::OList ls::OName
> rep::OName abs::OName n::os,...}) = let
> - val ls = unONamels ls
> - val sorted = Lib.sort (Lib.curry (Lib.equal LESS o String.compare)) ls
> - val s = let fun f (a,a',s) = if a = a' then s else let
> - val a = Type.mk_vartype a
> - val a' = Type.mk_vartype a'
> - val op |-> = Lib.|-> infix |->
> - in (a |-> a')::(a' |-> a)::s end
> - in ListPair.foldlEq f [] (ls,sorted) end
> - val th = Thm.INST_TYPE s th
> - val Pt = Thm.concl th
> - val (P,t) = Term.dest_comb(Pt)
> - val th = Thm.EXISTS(boolSyntax.mk_exists(t,Pt),t) th
> - val tyax = Definition.new_type_definition(n,th)
> - val th = Drule.define_new_type_bijections
> {name=n^"_repfns",ABS=abs,REP=rep,tyax=tyax}
> - val th1 = Drule.SPEC_ALL (Thm.CONJUNCT1 th)
> - val th2 = Drule.SPEC_ALL (Thm.CONJUNCT2 th)
> - in st_(OThm th2::OThm th1::OConst rep::OConst abs::OTypeOp n::os,st) end
> - | f EqMp (st as {stack=OThm fg::OThm f::os,...}) =
> st_(OThm(Thm.EQ_MP fg f)::os,st)
> - | f Nil st = push(OList [],st)
> - | f OpType (st as {stack=OList ls::OTypeOp t::os,...}) =
> st_(OType(find_type(t,ls))::os,st)
> - | f Pop (st as {stack=x::os,...}) = st_(os,st)
> - | f Ref (st as {stack=ONum k::os,dict,...}) =
> st_(Map.find(dict,k)::os,st)
> - | f Refl (st as {stack=OTerm t::os,...}) =
> st_(OThm(Thm.REFL t)::os,st)
> - | f Remove {stack=ONum k::os,dict,thms} = let
> +fun raw_read_article {tyop_from_ot,const_from_ot} input
> {tyops,consts,axioms} = let
> + val ERR = ERR "read_article"
> + fun unOTermls c = List.map (fn OTerm t => t | _ => raise ERR (c^"
> failed to pop a list of terms"))
> + fun unOTypels c = List.map (fn OType t => t | _ => raise ERR (c^"
> failed to pop a list of types"))
> + fun ot_to_const c s = Map.find(const_from_ot,s)
> + handle Map.NotFound => raise ERR (c^": no map from "^s^" to a constant")
> + fun ot_to_tyop c s = Map.find(tyop_from_ot ,s)
> + handle Map.NotFound => raise ERR (c^": no map from "^s^" to a type operator")
> + fun f "absTerm"(st as {stack=OTerm b::OVar v::os,...}) =
> st_(OTerm(mk_abs(v,b))::os,st)
> + | f "absThm" (st as {stack=OThm th::OVar v::os,...}) =
> (st_(OThm(absThm(v,th))::os,st)
> + handle HOL_ERR e => raise ERR ("absThm: failed with "^format_ERR e))
> + | f "appTerm"(st as {stack=OTerm x::OTerm f::os,...})=
> st_(OTerm(mk_comb(f,x))::os,st)
> + | f "appThm" (st as {stack=OThm xy::OThm fg::os,...})= let
> + val (f,g) = dest_eq(concl fg)
> + val (x,y) = dest_eq(concl xy)
> + val fxgx = AP_THM fg x
> + val gxgy = AP_TERM g xy
> + in st_(OThm(TRANS fxgx gxgy)::os,st) end
> + | f "assume" (st as {stack=OTerm t::os,...}) =
> st_(OThm(ASSUME t)::os,st)
> + | f "axiom" (st as {stack=OTerm t::OList ts::os,thms,...})
> = st_(OThm(axioms thms (unOTermls "axiom" ts,t))::os,st)
> + | f "betaConv" (st as {stack=OTerm t::os,...}) =
> st_(OThm(BETA_CONV t)::os,st)
> + | f "cons" (st as {stack=OList t::h::os,...}) =
> st_(OList(h::t)::os,st)
> + | f "const" (st as {stack=OName n::os,...}) =
> st_(OConst (ot_to_const "const" n)::os,st)
> + | f "constTerm" (st as {stack=OType Ty::OConst {Thy,Name}::os,...})
> + = st_(OTerm(mk_thy_const
> {Ty=Ty,Thy=Thy,Name=Name})::os,st)
> + | f "deductAntisym"(st as {stack=OThm t1::OThm t2::os,...}) =
> st_(OThm(DEDUCT_ANTISYM t1 t2)::os,st)
> + | f "def" {stack=ONum k::x::os,dict,thms} =
> {stack=x::os,dict=Map.insert(dict,k,x),thms=thms}
> + | f "defineConst" (st as {stack=OTerm t::OName n::os,...}) = let
> + val {const,def} = Map.find(consts,n) t
> + handle Map.NotFound => raise ERR ("defineConst: no map from
> "^n^" to a definition function")
> + in st_(OThm def::OConst const::os,st) end
> + | f "defineTypeOp" (st as {stack=OThm th::OList ls::OName
> rep::OName abs::OName n::os,...}) = let
> + val ls = List.map (fn OName s => mk_vartype s | _ => raise
> ERR "defineTypeOp failed to pop a list of names") ls
> + val {abs,rep,abs_rep,rep_abs,tyop} = Map.find(tyops,n)
> {axiom=th,args=ls,rep=rep,abs=abs}
> + val {Thy,Name,...} = dest_thy_const rep val rep = {Thy=Thy,Name=Name}
> + val {Thy,Name,...} = dest_thy_const abs val abs = {Thy=Thy,Name=Name}
> + in st_(OThm rep_abs::OThm abs_rep::OConst rep::OConst
> abs::OTypeOp tyop::os,st) end
> + | f "eqMp" (st as {stack=OThm f::OThm fg::os,...}) =
> (st_(OThm(EQ_MP fg f)::os,st)
> + handle HOL_ERR _ => raise ERR ("EqMp failed on "^thm_to_string
> fg^" and "^thm_to_string f))
> + | f "nil" st =
> push(OList [],st)
> + | f "opType" (st as {stack=OList ls::OTypeOp {Thy,Tyop}::os,...})
> + =
> st_(OType(mk_thy_type{Thy=Thy,Tyop=Tyop,Args=unOTypels "opType"
> ls})::os,st)
> + | f "pop" (st as {stack=x::os,...}) = st_(os,st)
> + | f "ref" (st as {stack=ONum k::os,dict,...}) =
> st_(Map.find(dict,k)::os,st)
> + | f "refl" (st as {stack=OTerm t::os,...}) =
> st_(OThm(REFL t)::os,st)
> + | f "remove" {stack=ONum k::os,dict,thms} = let
> val (dict,x) = Map.remove(dict,k)
> in {stack=x::os,dict=dict,thms=thms} end
> - | f Subst (st as {stack=OThm th::OList[OList tys,OList
> tms]::os,...}) = let
> - val tys = List.map (fn OList [OName a, OType t] =>
> {redex=Type.mk_vartype a, residue=t}) tys
> - val tms = List.map (fn OList [OVar v, OTerm t] => {redex=v,
> residue=t}) tms
> - val th = Thm.INST_TYPE tys th
> - val th = Thm.INST tms th
> + | f "subst" (st as {stack=OThm th::OList[OList tys,OList
> tms]::os,...}) = let
> + val tys = List.map (fn OList [OName a, OType t] =>
> {redex=mk_vartype a, residue=t}
> + | _ => raise ERR "subst failed to pop a
> list of [name,type] pairs") tys
> + val tms = List.map (fn OList [OVar v, OTerm t] => {redex=v, residue=t}
> + | _ => raise ERR "subst failed to pop a
> list of [var,term] pairs") tms
> + val th = INST_TYPE tys th
> + val th = INST tms th
> in st_(OThm th::os,st) end
> - | f Thm {stack=OTerm c::OList ls::OThm th::os,dict,thms} = let
> - val th = Thm.EQ_MP (Thm.ALPHA (Thm.concl th) c) th
> + | f "thm" {stack=OTerm c::OList ls::OThm th::os,dict,thms} = let
> + val th = EQ_MP (ALPHA (concl th) c) th
> + handle HOL_ERR _ => raise ERR "thm: desired conclusion not
> alpha-equivalent to theorem's conclusion"
> fun ft (OTerm h, th) = let
> - val c = Thm.concl th
> - val th = Thm.DISCH h th
> - val c' = Thm.concl th
> + val c = concl th
> + val th = DISCH h th
> + val c' = concl th
> in
> - if Term.aconv c c' then
> + if aconv c c' then
> Drule.ADD_ASSUM h th
> else let
> val (h',_) = boolSyntax.dest_imp c'
> - val h'h = Thm.ALPHA h' h
> + val h'h = ALPHA h' h
> val th = Drule.SUBS_OCCS [([1],h'h)] th
> in Drule.UNDISCH th end
> - end
> + end | ft _ = raise ERR "thm failed to pop a list of terms"
> val th = List.foldl ft th ls
> - in {stack=os,dict=dict,thms=th::thms} end
> - | f TypeOp (st as {stack=OName n::os,...}) =
> st_(OTypeOp n::os,st)
> - | f Var (st as {stack=OType t::OName n::os,...}) =
> st_(OVar(Term.mk_var(n,t))::os,st)
> - | f VarTerm (st as {stack=OVar t::os,...}) = st_(OTerm t::os,st)
> - | f VarType (st as {stack=OName n::os,...}) =
> st_(OType(Type.mk_vartype n)::os,st)
> - fun stripnl s = let open Substring in string(trimr 1 (full s)) end
> - fun loop x = case TextIO.inputLine file of
> - NONE => x before TextIO.closeIn(file)
> - | SOME line => loop (f (parse_line (stripnl line)) x handle Comment => x)
> -in #thms (loop {stack=[],dict=Map.mkDict(Int.compare),thms=[]}) end
> + in {stack=os,dict=dict,thms=Net.insert(concl th,th)thms} end
> + | f "typeOp" (st as {stack=OName n::os,...}) =
> st_(OTypeOp (ot_to_tyop "typeOp" n)::os,st)
> + | f "var" (st as {stack=OType t::OName n::os,...}) =
> st_(OVar(mk_var(n,t))::os,st)
> + | f "varTerm" (st as {stack=OVar t::os,...}) =
> st_(OTerm t::os,st)
> + | f "varType" (st as {stack=OName n::os,...}) =
> st_(OType(mk_vartype n)::os,st)
> + | f s st = let val c = String.sub(s,0) open Char Option Int
> + in if c = #"\"" then push(OName(valOf(String.fromString (trimlr
> s))),st) else
> + if isDigit c then push(ONum(valOf(fromString s)),st) else
> + if c = #"#" then st else
> + raise ERR ("Unknown command: "^s)
> + end
> + fun loop x = case TextIO.inputLine input of
> + NONE => x before TextIO.closeIn(input)
> + | SOME line => loop (f (trimr line) x)
> +in Net.listItems (#thms (loop
> {stack=[],dict=Map.mkDict(Int.compare),thms=Net.empty})) end
> +
> +fun read_article s r =
> + raw_read_article
> + {tyop_from_ot=tyop_from_ot(),
> + const_from_ot=const_from_ot()}
> + (TextIO.openIn s) r
> end
>
> Modified: HOL/src/opentheory/selftest.sml
> ===================================================================
> --- HOL/src/opentheory/selftest.sml 2011-01-10 06:01:44 UTC (rev 8844)
> +++ HOL/src/opentheory/selftest.sml 2011-01-10 17:32:29 UTC (rev 8845)
> @@ -1,17 +1,63 @@
> -open Opentheory
> +open Opentheory boolTheory boolLib bossLib HolKernel
> fun cmd pkg out = ("opentheory info --article -o "^out^" "^pkg)
> -val pkg = "bool-def-1.0"
> -val tmp = OS.FileSys.tmpName()
> -val _ = if OS.Process.isSuccess(Systeml.system_ps (cmd pkg tmp)) then let
> -val thms = read_article (TextIO.openIn tmp) {
> - thms=empty_thms,
> +val pkg = "bool-1.0"
> +(*
> +show: "Data.Bool"
> +input type operators: -> bool
> +input constants: = select
> +assumptions:
> +defined constants: ! /\ ==> ? ?! \/ ~ cond let F T
> +axioms:
> + |- !t. (\x. t x) = t
> + |- !P x. P x ==> P ((select) P)
> +
> types=typesFromList
> [("bool",fn [] => Type.bool),
> ("->",fn ls => Type.mk_type("fun",ls))],
> consts=constsFromList
> [("=",fn ty => Term.mk_const("=",ty)),
> - ("Data.Bool.select",fn ty => Term.mk_const("@",ty))]}
> -val thms = thmsFromList thms
> + ("Data.Bool.select",fn ty => Term.mk_const("@",ty))]
> +*)
> +val tmp = OS.FileSys.tmpName()
> +val _ = if OS.Process.isSuccess(Systeml.system_ps (cmd pkg tmp)) then let
> +val input = TextIO.openIn tmp
> +val tyop_from_ot = Redblackmap.fromList String.compare [
> + ("bool",{Thy="min",Tyop="bool"}),
> + ("->",{Thy="min",Tyop="fun"})]
> +val const_from_ot = Redblackmap.fromList String.compare [
> + ("=",{Thy="min",Name="="}),
> + ("Data.Bool.select",{Thy="min",Name="@"})]
> +val A = INST_TYPE[alpha|->mk_vartype"A",beta|->mk_vartype"B"]
> +val reader = {
> + tyops=Redblackmap.mkDict String.compare,
> + consts=
> + Redblackmap.fromList String.compare [
> + ("Data.Bool.!", fn _ => {const={Thy="bool",Name="!"},def=A FORALL_DEF}),
> + ("Data.Bool./\\", let
> + val th = prove(``$/\ = \p q. (\f. f p q) =
> \f:bool->bool->bool. f T T``,
> + SRW_TAC [][AND_DEF,FUN_EQ_THM] THEN EQ_TAC
> THEN SRW_TAC [][])
> + in fn _ => {const={Thy="bool",Name="/\\"},def=th} end),
> + ("Data.Bool.==>",let
> + val th = METIS_PROVE [] ``$==> = \p q. p /\ q <=> p``
> + in fn _ => {const={Thy="min",Name="==>"},def=th} end),
> + ("Data.Bool.?", let
> + val th = prove(``$? = \P. !q. (!x. P x ==> q) ==> q``,
> + SRW_TAC [][EXISTS_DEF,FUN_EQ_THM,EQ_IMP_THM] THEN
> + FIRST_X_ASSUM MATCH_MP_TAC THEN METIS_TAC [SELECT_AX])
> + in fn _ => {const={Thy="bool",Name="?"},def=A th} end),
> + ("Data.Bool.?!", fn _ => {const={Thy="bool",Name="?!"},def=A
> EXISTS_UNIQUE_DEF}),
> + ("Data.Bool.\\/", fn _ => {const={Thy="bool",Name="\\/"},def=OR_DEF}),
> + ("Data.Bool.~", fn _ => {const={Thy="bool",Name="~"},def=NOT_DEF}),
> + ("Data.Bool.cond", fn _ =>
> {const={Thy="bool",Name="COND"},def=A COND_DEF}),
> + ("Data.Bool.let", fn _ => {const={Thy="bool",Name="LET"},def=A LET_DEF}),
> + ("Data.Bool.F", fn _ => {const={Thy="bool",Name="F"},def=F_DEF}),
> + ("Data.Bool.T", fn _ => {const={Thy="bool",Name="T"},def=T_DEF})],
> + axioms=let open List Net Thm
> + fun ins th = insert(concl th,th)
> + val n = ins (A ETA_AX) (ins (A SELECT_AX) empty)
> + fun f _ (_,c) = hd (index c n)
> + in f end }
> +val thms = raw_read_article {tyop_from_ot=tyop_from_ot,
> const_from_ot=const_from_ot} input reader
> (* TODO: check that thms is the same set that opentheory
> says the package should have produced *)
> in () end else ()
>
>
> This was sent by the SourceForge.net collaborative development
> platform, the world's largest Open Source development site.
>
> ------------------------------------------------------------------------------
> Gaining the trust of online customers is vital for the success of any company
> that requires sensitive data to be transmitted over the Web. Learn how to
> best implement a security strategy that keeps consumers' information secure
> and instills the confidence they need to proceed with transactions.
> http://p.sf.net/sfu/oracle-sfdevnl
> _______________________________________________
> Hol-checkins mailing list
> Hol-checkins at lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-checkins
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
More information about the opentheory-users
mailing list