Commit e06b2459 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

petit nettoyage des AST et du parser

parent c50d0346
...@@ -191,24 +191,24 @@ uqualid: ...@@ -191,24 +191,24 @@ uqualid:
; ;
decl: decl:
| external_ LOGIC list1_ident_sep_comma COLON logic_type | LOGIC list1_lident_sep_comma COLON logic_type
{ Logic (loc_i 3, $1, $3, $5) } { Logic (loc_i 3, $2, $4) }
| AXIOM ident COLON lexpr | AXIOM ident COLON lexpr
{ Axiom (loc (), $2, $4) } { Axiom (loc (), $2, $4) }
| PREDICATE ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr | PREDICATE lident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR EQUAL lexpr
{ Predicate_def (loc (), $2, $4, $7) } { Predicate_def (loc (), $2, $4, $7) }
| INDUCTIVE ident COLON logic_type inddefn | INDUCTIVE lident COLON logic_type inddefn
{ Inductive_def (loc (), $2, $4, $5) } { Inductive_def (loc (), $2, $4, $5) }
| FUNCTION ident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON | FUNCTION lident LEFTPAR list0_logic_binder_sep_comma RIGHTPAR COLON
primitive_type EQUAL lexpr primitive_type EQUAL lexpr
{ Function_def (loc (), $2, $4, $7, $9) } { Function_def (loc (), $2, $4, $7, $9) }
| GOAL ident COLON lexpr | GOAL ident COLON lexpr
{ Goal (loc (), $2, $4) } { Goal (loc (), $2, $4) }
| EXTERNAL TYPE typedecl | TYPE typedecl
{ let loc, vl, id = $3 in TypeDecl (loc, true, vl, id) } { let loc, vl, id = $2 in TypeDecl (loc, 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 list1_uident_sep_comma
{ Uses (loc (), $2) } { Uses (loc (), $2) }
; ;
...@@ -220,22 +220,22 @@ list1_theory: ...@@ -220,22 +220,22 @@ list1_theory:
; ;
theory: theory:
| THEORY ident list0_decl END | THEORY uident list0_decl END
{ Theory ({ th_loc = loc (); th_name = $2; th_decl = $3 }) } { Theory ({ th_loc = loc (); th_name = $2; th_decl = $3 }) }
; ;
typedecl: typedecl:
| ident | lident
{ (loc_i 1, [], $1) } { (loc_i 1, [], $1) }
| type_var ident | type_var lident
{ (loc_i 2, [$1], $2) } { (loc_i 2, [$1], $2) }
| LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR ident | LEFTPAR type_var COMMA list1_type_var_sep_comma RIGHTPAR lident
{ (loc_i 6, $2 :: $4, $6) } { (loc_i 6, $2 :: $4, $6) }
; ;
typedefn: typedefn:
| /* epsilon */ | /* epsilon */
{ fun loc vl id -> TypeDecl (loc, false, vl, id) } { fun loc vl id -> TypeDecl (loc, vl, id) }
| EQUAL bar_ typecases typecont | EQUAL bar_ typecases typecont
{ fun loc vl id -> AlgType ((loc, vl, id, $3) :: $4) } { fun loc vl id -> AlgType ((loc, vl, id, $3) :: $4) }
; ;
...@@ -285,13 +285,13 @@ primitive_type: ...@@ -285,13 +285,13 @@ primitive_type:
{ PPTunit } { PPTunit }
*/ */
| type_var | type_var
{ PPTvarid $1 } { PPTtyvar $1 }
| lqualid | lqualid
{ PPTexternal ([], $1) } { PPTtyapp ([], $1) }
| primitive_type lqualid | primitive_type lqualid
{ PPTexternal ([$1], $2) } { PPTtyapp ([$1], $2) }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid | LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
{ PPTexternal ($2 :: $4, $6) } { PPTtyapp ($2 :: $4, $6) }
/* /*
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR | LEFTPAR list1_primitive_type_sep_comma RIGHTPAR
{ match $2 with [p] -> p | _ -> raise Parse_error } { match $2 with [p] -> p | _ -> raise Parse_error }
...@@ -331,7 +331,7 @@ list1_logic_binder_sep_comma: ...@@ -331,7 +331,7 @@ list1_logic_binder_sep_comma:
; ;
logic_binder: logic_binder:
| ident COLON primitive_type | lident COLON primitive_type
{ (loc_i 1, $1, $3) } { (loc_i 1, $1, $3) }
/*** /***
| ident COLON primitive_type ARRAY | ident COLON primitive_type ARRAY
...@@ -379,7 +379,7 @@ lexpr: ...@@ -379,7 +379,7 @@ 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_lident_sep_comma COLON primitive_type triggers
DOT lexpr %prec prec_forall DOT lexpr %prec prec_forall
{ let rec mk = function { let rec mk = function
| [] -> assert false | [] -> assert false
...@@ -387,7 +387,7 @@ lexpr: ...@@ -387,7 +387,7 @@ lexpr:
| 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 DOT lexpr %prec prec_exists | EXISTS lident 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)) }
...@@ -405,7 +405,7 @@ lexpr: ...@@ -405,7 +405,7 @@ lexpr:
{ $2 } { $2 }
| ident_or_string COLON lexpr %prec prec_named | ident_or_string COLON lexpr %prec prec_named
{ mk_pp (PPnamed ($1, $3)) } { mk_pp (PPnamed ($1, $3)) }
| LET ident EQUAL lexpr IN lexpr | LET lident EQUAL lexpr IN lexpr
{ mk_pp (PPlet ($2, $4, $6)) } { mk_pp (PPlet ($2, $4, $6)) }
| MATCH lexpr WITH bar_ match_cases END | MATCH lexpr WITH bar_ match_cases END
{ mk_pp (PPmatch ($2, $5)) } { mk_pp (PPmatch ($2, $5)) }
...@@ -485,6 +485,16 @@ list1_ident_sep_comma: ...@@ -485,6 +485,16 @@ list1_ident_sep_comma:
| ident COMMA list1_ident_sep_comma { $1 :: $3 } | ident COMMA list1_ident_sep_comma { $1 :: $3 }
; ;
list1_lident_sep_comma:
| lident { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;
list1_uident_sep_comma:
| uident { [$1] }
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
;
/******* programs ************************************************** /******* programs **************************************************
list0_ident_sep_comma: list0_ident_sep_comma:
......
...@@ -42,15 +42,9 @@ type qualid = ...@@ -42,15 +42,9 @@ type qualid =
| Qident of ident | Qident of ident
| Qdot of qualid * ident | Qdot of qualid * ident
type ppure_type = type pty =
(* | PPTtyvar of ident
| PPTint | PPTtyapp of pty list * qualid
| PPTbool
| PPTreal
| PPTunit
*)
| PPTvarid of ident
| PPTexternal of ppure_type list * qualid
type lexpr = type lexpr =
{ pp_loc : loc; pp_desc : pp_desc } { pp_loc : loc; pp_desc : pp_desc }
...@@ -64,19 +58,17 @@ and pp_desc = ...@@ -64,19 +58,17 @@ and pp_desc =
| PPinfix of lexpr * pp_infix * lexpr | PPinfix of lexpr * pp_infix * lexpr
| PPprefix of pp_prefix * lexpr | PPprefix of pp_prefix * lexpr
| PPif of lexpr * lexpr * lexpr | PPif of lexpr * lexpr * lexpr
| PPforall of ident * ppure_type * lexpr list list * lexpr | PPforall of ident * pty * lexpr list list * lexpr
| PPexists of ident * ppure_type * lexpr | PPexists of ident * pty * lexpr
| PPnamed of string * lexpr | PPnamed of string * lexpr
| PPlet of ident* lexpr * lexpr | PPlet of ident* lexpr * lexpr
| PPmatch of lexpr * ((qualid * ident list * loc) * lexpr) list | PPmatch of lexpr * ((qualid * ident list * loc) * lexpr) list
(*s Declarations. *) (*s Declarations. *)
type external_ = bool
type plogic_type = type plogic_type =
| PPredicate of ppure_type list | PPredicate of pty list
| PFunction of ppure_type list * ppure_type | PFunction of pty list * pty
type uses = ident type uses = ident
...@@ -87,16 +79,14 @@ type theory = { ...@@ -87,16 +79,14 @@ type theory = {
} }
and logic_decl = and logic_decl =
| Logic of loc * external_ * ident list * plogic_type | Logic of loc * ident list * plogic_type
| Predicate_def of loc * ident * (loc * ident * ppure_type) list * lexpr | Predicate_def of loc * ident * (loc * ident * pty) list * lexpr
| Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list | Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
| Function_def | Function_def of loc * ident * (loc * ident * pty) list * pty * lexpr
of loc * ident * (loc * ident * ppure_type) list * ppure_type * lexpr
| Axiom of loc * ident * lexpr | Axiom of loc * ident * lexpr
| Goal of loc * ident * lexpr | Goal of loc * ident * lexpr
| TypeDecl of loc * external_ * ident list * ident | TypeDecl of loc * ident list * ident
| AlgType of (loc * ident list * ident | AlgType of (loc * ident list * ident * (loc * ident * pty list) list) list
* (loc * ident * ppure_type list) list) list
| Theory of theory | Theory of theory
| Uses of loc * uses list | Uses of loc * uses list
......
...@@ -51,7 +51,7 @@ theory Eq ...@@ -51,7 +51,7 @@ theory Eq
end end
theory set theory Set
type elt type elt
...@@ -72,7 +72,7 @@ theory set ...@@ -72,7 +72,7 @@ theory set
end end
theory test theory Test
uses Eq, List uses Eq, List
......
...@@ -265,9 +265,9 @@ let rec qloc = function ...@@ -265,9 +265,9 @@ let rec qloc = function
(* parsed types -> intermediate types *) (* parsed types -> intermediate types *)
let rec dty env = function let rec dty env = function
| PPTvarid {id=x} -> | PPTtyvar {id=x} ->
Tyvar (find_user_type_var x env) Tyvar (find_user_type_var x env)
| PPTexternal (p, x) -> | PPTtyapp (p, x) ->
let loc = qloc x in let loc = qloc x in
let s, tv = let s, tv =
try specialize_tysymbol x env try specialize_tysymbol x env
...@@ -429,7 +429,7 @@ and fmla env = function ...@@ -429,7 +429,7 @@ and fmla env = function
open Ptree open Ptree
let add_type loc ext sl s env = let add_type loc sl s env =
if M.mem s.id env.tysymbols then error ~loc (ClashType s.id); if M.mem s.id env.tysymbols then error ~loc (ClashType s.id);
let tyvars = ref M.empty in let tyvars = ref M.empty in
let add_ty_var {id=x} = let add_ty_var {id=x} =
...@@ -473,11 +473,11 @@ let axiom loc s f env = ...@@ -473,11 +473,11 @@ let axiom loc s f env =
env env
let rec add_decl env = function let rec add_decl env = function
| TypeDecl (loc, ext, sl, s) -> | TypeDecl (loc, sl, s) ->
add_type loc ext sl s env add_type loc sl s env
| Logic (loc, ext, ids, PPredicate pl) -> | Logic (loc, ids, PPredicate pl) ->
List.fold_left (add_predicate loc pl) env ids List.fold_left (add_predicate loc pl) env ids
| Logic (loc, ext, ids, PFunction (pl, t)) -> | Logic (loc, ids, PFunction (pl, t)) ->
List.fold_left (add_function loc pl t) env ids List.fold_left (add_function loc pl t) env ids
| Axiom (loc, s, f) -> | Axiom (loc, s, f) ->
axiom loc s f env axiom loc s f 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