uses = declaration comme une autre ; retablissement du . dans la syntaxe de forall/exists

parent 644ef011
...@@ -2,14 +2,7 @@ ...@@ -2,14 +2,7 @@
syntaxe syntaxe
------- -------
- le point (.) dans les noms qualifiés introduit un conflit dans la syntaxe - open
de forall/exists
forall x : a. b
forall x : a.b: c
-> changement temporaire de syntaxe pour forall / exists : virgule
plutôt que point
sémantique sémantique
...@@ -17,3 +10,7 @@ s ...@@ -17,3 +10,7 @@ s
- uses : pour l'instant, l'ordre des théories dans le fichier est important - uses : pour l'instant, l'ordre des théories dans le fichier est important
i.e. les théories mentionnées par uses doivent être définies précédemment i.e. les théories mentionnées par uses doivent être définies précédemment
- open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
de même nom)
...@@ -208,6 +208,8 @@ decl: ...@@ -208,6 +208,8 @@ decl:
{ let loc, vl, id = $3 in TypeDecl (loc, true, vl, id) } { let loc, vl, id = $3 in TypeDecl (loc, true, vl, id) }
| TYPE typedecl typedefn | TYPE typedecl typedefn
{ let loc, vl, id = $2 in $3 loc vl id } { let loc, vl, id = $2 in $3 loc vl id }
| USES list1_ident_sep_comma
{ Uses (loc (), $2) }
; ;
list1_theory: list1_theory:
...@@ -218,15 +220,8 @@ list1_theory: ...@@ -218,15 +220,8 @@ list1_theory:
; ;
theory: theory:
| THEORY ident uses list0_decl END | THEORY ident list0_decl END
{ Theory ({ th_loc = loc (); th_name = $2; th_uses = $3; th_decl = $4 }) } { Theory ({ th_loc = loc (); th_name = $2; th_decl = $3 }) }
;
uses:
| /* epsilon */
{ [] }
| USES list1_ident_sep_comma
{ $2 }
; ;
typedecl: typedecl:
...@@ -385,14 +380,14 @@ lexpr: ...@@ -385,14 +380,14 @@ lexpr:
| IF lexpr THEN lexpr ELSE lexpr %prec prec_if | IF lexpr THEN lexpr ELSE lexpr %prec prec_if
{ mk_pp (PPif ($2, $4, $6)) } { mk_pp (PPif ($2, $4, $6)) }
| FORALL list1_ident_sep_comma COLON primitive_type triggers | FORALL list1_ident_sep_comma COLON primitive_type triggers
COMMA lexpr %prec prec_forall DOT lexpr %prec prec_forall
{ let rec mk = function { let rec mk = function
| [] -> assert false | [] -> assert false
| [id] -> mk_pp (PPforall (id, $4, $5, $7)) | [id] -> mk_pp (PPforall (id, $4, $5, $7))
| id :: l -> mk_pp (PPforall (id, $4, [], mk l)) | id :: l -> mk_pp (PPforall (id, $4, [], mk l))
in in
mk $2 } mk $2 }
| EXISTS ident COLON primitive_type COMMA lexpr %prec prec_exists | EXISTS ident COLON primitive_type DOT lexpr %prec prec_exists
{ mk_pp (PPexists ($2, $4, $6)) } { mk_pp (PPexists ($2, $4, $6)) }
| INTEGER | INTEGER
{ mk_pp (PPconst (ConstInt $1)) } { mk_pp (PPconst (ConstInt $1)) }
......
...@@ -83,7 +83,6 @@ type uses = ident ...@@ -83,7 +83,6 @@ type uses = ident
type theory = { type theory = {
th_loc : loc; th_loc : loc;
th_name : ident; th_name : ident;
th_uses : uses list;
th_decl : logic_decl list; th_decl : logic_decl list;
} }
...@@ -99,5 +98,7 @@ and logic_decl = ...@@ -99,5 +98,7 @@ and logic_decl =
| AlgType of (loc * ident list * ident | AlgType of (loc * ident list * ident
* (loc * ident * ppure_type list) list) list * (loc * ident * ppure_type list) list) list
| Theory of theory | Theory of theory
| Uses of loc * uses list
type logic_file = logic_decl list type logic_file = logic_decl list
(* test file *) (* test file *)
theory A
type t
logic c:t
end
theory B
uses A
logic d : A.t
logic p : A.t -> prop
end
theory C
uses B
logic e : B.A.t
axiom test : B.p(B.A.c)
end
theory Int theory Int
type int type int
...@@ -9,8 +31,6 @@ end ...@@ -9,8 +31,6 @@ end
theory List theory List
uses Int
type 'a list type 'a list
logic nil : 'a list logic nil : 'a list
...@@ -19,6 +39,8 @@ theory List ...@@ -19,6 +39,8 @@ theory List
logic is_nil : 'a list -> prop logic is_nil : 'a list -> prop
uses Int
logic length : 'a list -> Int.int logic length : 'a list -> Int.int
end end
...@@ -31,8 +53,6 @@ end ...@@ -31,8 +53,6 @@ end
theory set theory set
uses Eq
type elt type elt
type t type t
...@@ -41,11 +61,13 @@ theory set ...@@ -41,11 +61,13 @@ theory set
logic empty : t logic empty : t
axiom empty_def1 : forall x:elt, not in_(x, empty) axiom empty_def1 : forall x:elt. not in_(x, empty)
logic add : elt, t -> t logic add : elt, t -> t
axiom add_def1 : forall x,y:elt, forall s:t, uses Eq
axiom add_def1 : forall x,y:elt. forall s:t.
in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s)) in_(x, add(y, s)) <-> (Eq.eq(x, y) or in_(x, s))
end end
...@@ -54,7 +76,7 @@ theory test ...@@ -54,7 +76,7 @@ theory test
uses Eq, List uses Eq, List
axiom a : forall x : 'a, not Eq.eq(List.nil, List.cons(List.nil, List.nil)) axiom a : forall x : 'a. not Eq.eq(List.nil, List.cons(List.nil, List.nil))
end end
...@@ -483,6 +483,8 @@ let rec add_decl env = function ...@@ -483,6 +483,8 @@ let rec add_decl env = function
axiom loc s f env axiom loc s f env
| Theory th -> | Theory th ->
add_theory th env add_theory th env
| Uses (loc, uses) ->
List.fold_left add_global_theory env uses
| _ -> | _ ->
assert false (*TODO*) assert false (*TODO*)
...@@ -491,8 +493,7 @@ and add_decls env = List.fold_left add_decl env ...@@ -491,8 +493,7 @@ and add_decls env = List.fold_left add_decl env
and add_theory th env = and add_theory th env =
let id = th.th_name.id in let id = th.th_name.id in
if M.mem id env.theories then error ~loc:th.th_loc (ClashTheory id); if M.mem id env.theories then error ~loc:th.th_loc (ClashTheory id);
let th_env = List.fold_left add_global_theory empty th.th_uses in let th_env = add_decls empty th.th_decl in
let th_env = add_decls th_env th.th_decl in
Hashtbl.add loaded_theories id th_env; Hashtbl.add loaded_theories id th_env;
env env
......
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