goal/lemma/axiom

parent a5ad5423
......@@ -71,6 +71,7 @@
"inductive", INDUCTIVE;
(*"int", INT;*)
"invariant", INVARIANT;
"lemma", LEMMA;
"let", LET;
"logic", LOGIC;
"match", MATCH;
......
......@@ -101,7 +101,8 @@
%token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI
%token FUN FUNCTION GE GOAL GT
%token IF IMPORT IN INCLUDE INDUCTIVE INT INVARIANT
%token LE LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LET LOGIC LRARROW LT MATCH MINUS
%token LE LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA
%token LET LOGIC LRARROW LT MATCH MINUS
%token NAMESPACE NOT NOTEQ OF OR PARAMETER PERCENT PLUS PREDICATE PROP
%token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ
......@@ -259,11 +260,13 @@ decl:
| list1_logic_decl
{ Logic (loc (), $1) }
| AXIOM uident COLON lexpr
{ Axiom (loc (), $2, $4) }
{ Prop (loc (), Kaxiom, $2, $4) }
| GOAL uident COLON lexpr
{ Prop (loc (), Kgoal, $2, $4) }
| LEMMA uident COLON lexpr
{ Prop (loc (), Klemma, $2, $4) }
| INDUCTIVE lident COLON logic_type inddefn
{ Inductive_def (loc (), $2, $4, $5) }
| GOAL uident COLON lexpr
{ Goal (loc (), $2, $4) }
| USE use
{ Use (loc (), $2) }
| NAMESPACE uident list0_decl END
......
......@@ -104,12 +104,14 @@ type logic_decl = {
ld_def : lexpr option;
}
type prop_kind =
| Kaxiom | Klemma | Kgoal
type decl =
| TypeDecl of loc * type_decl list
| Logic of loc * logic_decl list
| Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
| Axiom of loc * ident * lexpr
| Goal of loc * ident * lexpr
| Prop of loc * prop_kind * ident * lexpr
| Use of loc * use
| Namespace of loc * ident * decl list
......
......@@ -694,6 +694,11 @@ let load_file file =
close_in c;
tl
let prop_kind = function
| Kaxiom -> Axiom
| Kgoal -> Goal
| Klemma -> Lemma
let rec find_theory env q = match q with
| Qident id ->
(* local theory *)
......@@ -734,8 +739,8 @@ and add_decl env th = function
add_types loc dl th
| Logic (loc, dl) ->
add_logics loc dl th
| Axiom (loc, s, f) ->
add_prop Theory.Axiom loc s f th
| Prop (loc, k, s, f) ->
add_prop (prop_kind k) loc s f th
| Use (loc, use) ->
let t = find_theory env use.use_theory in
let n = match use.use_as with
......@@ -765,7 +770,6 @@ and add_decl env th = function
let th = add_decls env th dl in
let n = id_user id id loc in
close_namespace th n ~import:false
| Goal _
| Inductive_def _ ->
assert false (*TODO*)
......
......@@ -18,6 +18,8 @@ theory B
use import prelude.List
type t
axiom Ax : forall x : t list. true
lemma L : forall x : t list. true
goal G : forall x : t list. true
end
(*
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment