symboles primitifs

parent f525847b
...@@ -3,8 +3,6 @@ ...@@ -3,8 +3,6 @@
theory Int theory Int
type int
logic (<) (int, int) logic (<) (int, int)
logic (<=)(int, int) logic (<=)(int, int)
logic (>) (int, int) logic (>) (int, int)
......
...@@ -324,15 +324,38 @@ let add_symbol add id v uc = ...@@ -324,15 +324,38 @@ let add_symbol add id v uc =
let get_namespace uc = List.hd uc.uc_import let get_namespace uc = List.hd uc.uc_import
(** Equality *) (** Builtin symbols *)
let t_int = create_tysymbol (id_fresh "int") [] None
let t_real = create_tysymbol (id_fresh "real") [] None
let eq = let eq =
let v = ty_var (create_tvsymbol (id_fresh "a")) in let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "eq") [v; v;] create_psymbol (id_fresh "=") [v; v;]
let neq =
let v = ty_var (create_tvsymbol (id_fresh "a")) in
create_psymbol (id_fresh "<>") [v; v;]
let builtin_tysymbols = [t_int; t_real]
let builtin_psymbols = [eq; neq]
let ts_name x = x.ts_name
let ps_name x = x.ps_name
let eq_th = id_register (id_fresh "Eq") let builtin_ns =
let add adder name = List.fold_right (fun s -> adder (name s).id_short s) in
let ns = add add_ts ts_name builtin_tysymbols empty_ns in
let ns = add add_ps ps_name builtin_psymbols ns in
ns
let builtin_th = id_register (id_fresh "Builtin")
let known_eq = Mid.add eq.ps_name eq_th Mid.empty let builtin_known =
let add name = List.fold_right (fun s -> Mid.add (name s) builtin_th) in
let kn = Mid.add builtin_th builtin_th Mid.empty in
let kn = add ts_name builtin_tysymbols kn in
let kn = add ps_name builtin_psymbols kn in
kn
(** Manage theories *) (** Manage theories *)
...@@ -340,8 +363,8 @@ let known_eq = Mid.add eq.ps_name eq_th Mid.empty ...@@ -340,8 +363,8 @@ let known_eq = Mid.add eq.ps_name eq_th Mid.empty
let create_theory n = { let create_theory n = {
uc_name = n; uc_name = n;
uc_param = Sid.empty; uc_param = Sid.empty;
uc_known = Mid.add n n known_eq; uc_known = Mid.add n n builtin_known;
uc_import = [empty_ns]; uc_import = [builtin_ns];
uc_export = [empty_ns]; uc_export = [empty_ns];
uc_decls = []; uc_decls = [];
} }
...@@ -511,6 +534,6 @@ let print_t fmt t = ...@@ -511,6 +534,6 @@ let print_t fmt t =
(* (*
Local Variables: Local Variables:
compile-command: "make -C .. test" compile-command: "make -C ../.. test"
End: End:
*) *)
...@@ -43,7 +43,6 @@ ...@@ -43,7 +43,6 @@
(fun (x,y) -> Hashtbl.add keywords x y) (fun (x,y) -> Hashtbl.add keywords x y)
[ "absurd", ABSURD; [ "absurd", ABSURD;
"and", AND; "and", AND;
(*"array", ARRAY;*)
"as", AS; "as", AS;
"assert", ASSERT; "assert", ASSERT;
"axiom", AXIOM; "axiom", AXIOM;
...@@ -69,7 +68,6 @@ ...@@ -69,7 +68,6 @@
"import", IMPORT; "import", IMPORT;
"in", IN; "in", IN;
"inductive", INDUCTIVE; "inductive", INDUCTIVE;
(*"int", INT;*)
"invariant", INVARIANT; "invariant", INVARIANT;
"lemma", LEMMA; "lemma", LEMMA;
"let", LET; "let", LET;
...@@ -85,7 +83,6 @@ ...@@ -85,7 +83,6 @@
"raise", RAISE; "raise", RAISE;
"raises", RAISES; "raises", RAISES;
"reads", READS; "reads", READS;
"real", REAL;
"rec", REC; "rec", REC;
"ref", REF; "ref", REF;
"returns", RETURNS; "returns", RETURNS;
...@@ -194,9 +191,7 @@ rule token = parse ...@@ -194,9 +191,7 @@ rule token = parse
{ LRARROW } { LRARROW }
| "=" | "="
{ EQUAL } { EQUAL }
| "<>" | "<>" | "<" | "<=" | ">" | ">=" as s
{ NOTEQ }
| "<" | "<=" | ">" | ">=" as s
{ INFIXOP0 s } { INFIXOP0 s }
| "+" | "+"
{ INFIXOP2 "+" } { INFIXOP2 "+" }
......
...@@ -101,11 +101,11 @@ ...@@ -101,11 +101,11 @@
%token DONE DOT ELSE END EOF EQUAL %token DONE DOT ELSE END EOF EQUAL
%token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI %token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI
%token FUN FUNCTION GOAL %token FUN FUNCTION GOAL
%token IF IMPORT IN INCLUDE INDUCTIVE INT INVARIANT %token IF IMPORT IN INCLUDE INDUCTIVE INVARIANT
%token LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA %token LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA
%token LET LOGIC LRARROW MATCH MINUS %token LET LOGIC LRARROW MATCH MINUS
%token NAMESPACE NOT NOTEQ OF OR PARAMETER PREDICATE PROP %token NAMESPACE NOT OF OR PARAMETER PREDICATE PROP
%token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB %token QUOTE RAISE RAISES READS REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ %token RIGHTPAR RIGHTSQ
%token SEMICOLON SLASH %token SEMICOLON SLASH
%token THEN THEORY TIMES TRUE TRY TYPE UNDERSCORE %token THEN THEORY TIMES TRUE TRY TYPE UNDERSCORE
...@@ -136,7 +136,7 @@ ...@@ -136,7 +136,7 @@
%right AND AMPAMP %right AND AMPAMP
%right NOT %right NOT
%right prec_if %right prec_if
%left EQUAL NOTEQ INFIXOP0 %left EQUAL INFIXOP0
%left INFIXOP2 MINUS %left INFIXOP2 MINUS
%left INFIXOP3 %left INFIXOP3
%right uminus %right uminus
...@@ -190,6 +190,7 @@ lident_infix: ...@@ -190,6 +190,7 @@ lident_infix:
| INFIXOP0 { $1 } | INFIXOP0 { $1 }
| INFIXOP2 { $1 } | INFIXOP2 { $1 }
| INFIXOP3 { $1 } | INFIXOP3 { $1 }
| EQUAL { "=" }
| MINUS { "-" } | MINUS { "-" }
...@@ -342,16 +343,6 @@ indcase: ...@@ -342,16 +343,6 @@ indcase:
; ;
primitive_type: primitive_type:
/*
| INT
{ PPTint }
| BOOL
{ PPTbool }
| REAL
{ PPTreal }
| UNIT
{ PPTunit }
*/
| type_var | type_var
{ PPTtyvar $1 } { PPTtyvar $1 }
| lqualid | lqualid
...@@ -383,9 +374,8 @@ lexpr: ...@@ -383,9 +374,8 @@ lexpr:
| NOT lexpr | NOT lexpr
{ prefix_pp PPnot $2 } { prefix_pp PPnot $2 }
| lexpr EQUAL lexpr | lexpr EQUAL lexpr
{ infix_pp $1 PPeq $3 } { let id = { id = "="; id_loc = loc_i 2 } in
| lexpr NOTEQ lexpr mk_pp (PPapp (Qident id, [$1; $3])) }
{ infix_pp $1 PPneq $3 }
| lexpr INFIXOP0 lexpr | lexpr INFIXOP0 lexpr
{ let id = { id = $2; id_loc = loc_i 2 } in { let id = { id = $2; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$1; $3])) } mk_pp (PPapp (Qident id, [$1; $3])) }
......
...@@ -32,7 +32,7 @@ type constant = ...@@ -32,7 +32,7 @@ type constant =
| ConstFloat of real_constant | ConstFloat of real_constant
type pp_infix = type pp_infix =
| PPand | PPor | PPimplies | PPiff | PPeq | PPneq | PPand | PPor | PPimplies | PPiff
type pp_prefix = type pp_prefix =
| PPneg | PPnot | PPneg | PPnot
......
...@@ -112,23 +112,6 @@ let report fmt = function ...@@ -112,23 +112,6 @@ let report fmt = function
| UnboundTypeVar s -> | UnboundTypeVar s ->
fprintf fmt "unbound type variable '%s" s fprintf fmt "unbound type variable '%s" s
(****
| OpenTheory ->
fprintf fmt "cannot open a new theory in a non-empty context"
| CloseTheory ->
fprintf fmt "cannot close theory: there are still unclosed namespaces"
| NoOpenedTheory ->
fprintf fmt "no opened theory"
| NoOpenedNamespace ->
fprintf fmt "no opened namespace"
| RedeclaredIdent id ->
fprintf fmt "cannot redeclare identifier %s" id.id_short
| CannotInstantiate ->
fprintf fmt "cannot instantiate a defined symbol"
****)
(** Environments *) (** Environments *)
...@@ -364,7 +347,6 @@ let binop = function ...@@ -364,7 +347,6 @@ let binop = function
| PPor -> For | PPor -> For
| PPimplies -> Fimplies | PPimplies -> Fimplies
| PPiff -> Fiff | PPiff -> Fiff
| _ -> assert false
let rec dterm env t = let rec dterm env t =
let n, ty = dterm_node t.pp_loc env t.pp_desc in let n, ty = dterm_node t.pp_loc env t.pp_desc in
...@@ -399,10 +381,10 @@ and dfmla env e = match e.pp_desc with ...@@ -399,10 +381,10 @@ and dfmla env e = match e.pp_desc with
Fnot (dfmla env a) Fnot (dfmla env a)
| PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) -> | PPinfix (a, (PPand | PPor | PPimplies | PPiff as op), b) ->
Fbinop (binop op, dfmla env a, dfmla env b) Fbinop (binop op, dfmla env a, dfmla env b)
| PPinfix (a, (PPeq | PPneq as op), b) -> (* | PPinfix (a, (PPeq | PPneq as op), b) -> *)
let s, _ = specialize_psymbol Theory.eq in (* let s, _ = specialize_psymbol Theory.eq in *)
let f = Fapp (s, [dterm env a; dterm env b]) in (* let f = Fapp (s, [dterm env a; dterm env b]) in *)
if op = PPeq then f else Fnot f (* if op = PPeq then f else Fnot f *)
| PPif (a, b, c) -> | PPif (a, b, c) ->
Fif (dfmla env a, dfmla env b, dfmla env c) Fif (dfmla env a, dfmla env b, dfmla env c)
| PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *) | PPforall ({id=x}, ty, _, a) -> (* TODO: triggers *)
...@@ -473,11 +455,13 @@ and fmla env = function ...@@ -473,11 +455,13 @@ and fmla env = function
open Ptree open Ptree
let add_types loc dl th = let add_types loc dl th =
let ns = get_namespace th in
let def = let def =
List.fold_left List.fold_left
(fun def d -> (fun def d ->
let id = d.td_ident in let id = d.td_ident in
if M.mem id.id def then error ~loc:id.id_loc (ClashType id.id); if M.mem id.id def || Mnm.mem id.id ns.ns_ts then
error ~loc:id.id_loc (ClashType id.id);
M.add id.id d def) M.add id.id d def)
M.empty dl M.empty dl
in in
......
...@@ -3,15 +3,16 @@ ...@@ -3,15 +3,16 @@
theory TestPrelude theory TestPrelude
use prelude.List use prelude.List
use list.IntList (* use list.IntList *)
use array.IntArray use array.IntArray
end end
theory A theory A
use import prelude.Int
type t type t
logic p(t) logic p(t)
logic q(x: t) = p(x) logic q(x: t) = p(x)
logic c : t logic c : real
end end
theory B theory B
......
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