[opentheory-users] Fwd: [Hol-checkins] SF.net SVN: hol:[8845] HOL/src/opentheory
Ramana Kumar
ramana.kumar at gmail.com
Mon Jan 10 17:35:30 UTC 2011
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
More information about the opentheory-users
mailing list