Commit 230a8485 authored by Andrei Paskevich's avatar Andrei Paskevich

labeled binding idents in logic and programs

parent ae1037fb
......@@ -274,6 +274,7 @@ let specialize_lsymbol ~loc s =
let ident_of_vs ~loc vs =
{ id = vs.vs_name.id_string;
id_lab = vs.vs_name.id_label;
id_loc = match vs.vs_name.id_origin with
| User loc -> loc
| _ -> loc }
......
......@@ -72,6 +72,10 @@
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
let mk_id id loc = { id = id; id_lab = []; id_loc = loc }
let add_lab id l = { id with id_lab = l }
let user_loc fname lnum bol cnum1 cnum2 =
let pos = {
Lexing.pos_fname = fname;
......@@ -164,9 +168,9 @@ list0_theory:
;
theory_head:
| THEORY uident
{ let id = $2 in
let name = Ident.id_user id.id id.id_loc in
| THEORY uident labels
{ let id = add_lab $2 $3 and labels = $3 in
let name = Ident.id_user ~labels id.id id.id_loc in
ref_push uc_ref (create_theory name); id }
;
......@@ -226,7 +230,7 @@ decl:
| META ident list1_meta_arg_sep_comma
{ Meta (loc (), $2, $3) }
| META STRING list1_meta_arg_sep_comma
{ Meta (loc (), { id = $2; id_loc = loc_i 2 }, $3) }
{ Meta (loc (), mk_id $2 (loc_i 2), $3) }
;
/* Use and clone */
......@@ -286,13 +290,14 @@ list1_type_decl:
;
type_decl:
| lident type_args typedefn
{ { td_loc = loc (); td_ident = $1; td_params = $2; td_def = $3 } }
| lident labels type_args typedefn
{ { td_loc = loc (); td_ident = add_lab $1 $2;
td_params = $3; td_def = $4 } }
;
type_args:
| /* epsilon */ { [] }
| type_var type_args { $1 :: $2 }
| type_var labels type_args { add_lab $1 $2 :: $3 }
;
typedefn:
......@@ -308,7 +313,7 @@ typecases:
;
typecase:
| uident params { (loc_i 1,$1,$2) }
| uident labels params { (loc (), add_lab $1 $2, $3) }
;
/* Logic declarations */
......@@ -319,9 +324,9 @@ list1_logic_decl:
;
logic_decl:
| lident_rich params logic_type_option logic_def_option
{ { ld_loc = loc (); ld_ident = $1; ld_params = $2;
ld_type = $3; ld_def = $4; } }
| lident_rich labels params logic_type_option logic_def_option
{ { ld_loc = loc (); ld_ident = add_lab $1 $2;
ld_params = $3; ld_type = $4; ld_def = $5 } }
;
logic_type_option:
......@@ -342,8 +347,9 @@ list1_inductive_decl:
;
inductive_decl:
| lident_rich params inddefn
{ { in_loc = loc (); in_ident = $1; in_params = $2; in_def = $3 } }
| lident_rich labels params inddefn
{ { in_loc = loc (); in_ident = add_lab $1 $2;
in_params = $3; in_def = $4 } }
;
inddefn:
......@@ -357,7 +363,7 @@ indcases:
;
indcase:
| uident COLON lexpr { (loc (),$1,$3) }
| uident labels COLON lexpr { (loc (), add_lab $1 $2, $4) }
;
/* Type expressions */
......@@ -414,36 +420,27 @@ lexpr:
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr ASYM_OR lexpr
{ let label = Ident.label "asym_split" in
mk_pp (PPnamed (label, infix_pp $1 PPor $3)) }
{ mk_pp (PPnamed (Ident.label "asym_split", infix_pp $1 PPor $3)) }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr ASYM_AND lexpr
{ let label = Ident.label "asym_split" in
mk_pp (PPnamed (label, infix_pp $1 PPand $3)) }
{ mk_pp (PPnamed (Ident.label "asym_split", infix_pp $1 PPand $3)) }
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
{ let id = { id = infix "="; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
{ mk_pp (PPinfix ($1, mk_id (infix "=") (loc_i 2), $3)) }
| lexpr LTGT lexpr
{ let id = { id = infix "="; id_loc = loc_i 2 } in
prefix_pp PPnot (mk_pp (PPinfix ($1, id, $3))) }
{ prefix_pp PPnot (mk_pp (PPinfix ($1, mk_id (infix "=") (loc_i 2), $3))) }
| lexpr OP1 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
{ mk_pp (PPinfix ($1, mk_id (infix $2) (loc_i 2), $3)) }
| lexpr OP2 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
{ mk_pp (PPinfix ($1, mk_id (infix $2) (loc_i 2), $3)) }
| lexpr OP3 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
{ mk_pp (PPinfix ($1, mk_id (infix $2) (loc_i 2), $3)) }
| lexpr OP4 lexpr
{ let id = { id = infix $2; id_loc = loc_i 2 } in
mk_pp (PPinfix ($1, id, $3)) }
{ mk_pp (PPinfix ($1, mk_id (infix $2) (loc_i 2), $3)) }
| any_op lexpr %prec prefix_op
{ let id = { id = prefix $1; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$2])) }
{ mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
| qualid list1_lexpr_arg
{ mk_pp (PPapp ($1, $2)) }
| IF lexpr THEN lexpr ELSE lexpr
......@@ -460,8 +457,8 @@ lexpr:
{ mk_pp (PPmatch ($2, $5)) }
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
{ mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
| EPSILON lident COLON primitive_type DOT lexpr
{ mk_pp (PPeps ($2, $4, $6)) }
| EPSILON lident labels COLON primitive_type DOT lexpr
{ mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
| lexpr COLON primitive_type
{ mk_pp (PPcast ($1, $3)) }
| lexpr_arg
......@@ -491,8 +488,7 @@ lexpr_arg:
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
{ mk_pp (PPtuple ($2 :: $4)) }
| OPPREF lexpr_arg
{ let id = { id = prefix $1; id_loc = loc_i 2 } in
mk_pp (PPapp (Qident id, [$2])) }
{ mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
;
quant:
......@@ -551,7 +547,7 @@ list1_pat_uni:
pat_uni:
| pat_arg { $1 }
| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident { mk_pat (PPpas ($1, $3)) }
| pat_uni AS lident labels { mk_pat (PPpas ($1, add_lab $3 $4)) }
;
list1_pat_arg:
......@@ -561,7 +557,7 @@ list1_pat_arg:
pat_arg:
| UNDERSCORE { mk_pat (PPpwild) }
| lident { mk_pat (PPpvar $1) }
| lident labels { mk_pat (PPpvar (add_lab $1 $2)) }
| uqualid { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR { $2 }
......@@ -613,6 +609,12 @@ list1_param_var_sep_comma:
param_var:
| list1_lident COLON primitive_type
{ List.map (fun id -> (Some id, $3)) $1 }
| list1_lident label labels list0_lident_labels COLON primitive_type
{ let l = match List.rev $1 with
| i :: l -> add_lab i ($2 :: $3) :: l
| [] -> assert false
in
List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
;
list1_lident:
......@@ -620,6 +622,11 @@ list1_lident:
| lident list1_lident { $1 :: $2 }
;
list0_lident_labels:
| /* epsilon */ { [] }
| lident labels list0_lident_labels { add_lab $1 $2 :: $3 }
;
/* Idents */
ident:
......@@ -636,17 +643,17 @@ lident_rich:
| lident
{ $1 }
| LEFTPAR lident_op RIGHTPAR
{ { id = infix $2; id_loc = loc () } }
{ mk_id (infix $2) (loc ()) }
| LEFTPAR_STAR_RIGHTPAR
{ { id = infix "*"; id_loc = loc () } }
{ mk_id (infix "*") (loc ()) }
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
{ { id = prefix $2; id_loc = loc () } }
{ mk_id (prefix $2) (loc ()) }
| LEFTPAR OPPREF RIGHTPAR
{ { id = prefix $2; id_loc = loc () } }
{ mk_id (prefix $2) (loc ()) }
;
lident:
| LIDENT { { id = $1; id_loc = loc () } }
| LIDENT { mk_id $1 (loc ()) }
;
lident_op:
......@@ -665,7 +672,7 @@ any_op:
;
uident:
| UIDENT { { id = $1; id_loc = loc () } }
| UIDENT { mk_id $1 (loc ()) }
;
lq_lident:
......@@ -713,6 +720,11 @@ label:
Ident.label ~loc $1 }
;
labels:
| /* epsilon */ { [] }
| label labels { $1 :: $2 }
;
bar_:
| /* epsilon */ { () }
| BAR { () }
......
......@@ -36,7 +36,7 @@ type pp_binop =
type pp_unop =
| PPnot
type ident = { id : string; id_loc : loc }
type ident = { id : string; id_lab : label list; id_loc : loc }
type qualid =
| Qident of ident
......
......@@ -460,7 +460,7 @@ and dterm_node loc env = function
let trl = List.map (List.map trigger) trl in
let id, ty, f = match trigger a with
| TRterm t ->
let id = { id = "fc" ; id_loc = loc } in
let id = { id = "fc"; id_lab = []; id_loc = loc } in
let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
uqu ([],t.dt_ty)
......@@ -473,7 +473,7 @@ and dterm_node loc env = function
in
id, ty, Fapp (ps_equ, [h;t])
| TRfmla f ->
let id = { id = "pc" ; id_loc = loc } in
let id = { id = "pc"; id_lab = []; id_loc = loc } in
let (uid,uty),uqu = match List.rev uqu with
| uq :: uqu -> uq, List.rev uqu
| [] -> assert false
......
......@@ -154,6 +154,8 @@ rule token = parse
{ comment lexbuf; token lexbuf }
| "'"
{ QUOTE }
| "`"
{ BACKQUOTE }
| ","
{ COMMA }
| "("
......
......@@ -34,6 +34,17 @@
let mk_pat p = { pat_loc = loc (); pat_desc = p }
let add_lab id l = { id with id_lab = l }
let user_loc fname lnum bol cnum1 cnum2 =
let pos = {
Lexing.pos_fname = fname;
Lexing.pos_lnum = lnum;
Lexing.pos_bol = bol;
Lexing.pos_cnum = cnum1 }
in
pos, { pos with Lexing.pos_cnum = cnum2 }
(* FIXME: factorize with parser/parser.mly *)
let infix s = "infix " ^ s
let prefix s = "prefix " ^ s
......@@ -57,23 +68,23 @@
mk_apply e
let mk_infix e1 op e2 =
let id = { id = infix op; id_loc = loc_i 2 } in
let id = { id = infix op; id_lab = []; id_loc = loc_i 2 } in
mk_expr (mk_apply_id id [e1; e2])
let mk_binop e1 op e2 =
let id = { id = op; id_loc = loc_i 2 } in
let id = { id = op; id_lab = []; id_loc = loc_i 2 } in
mk_expr (mk_apply_id id [e1; e2])
let mk_prefix op e1 =
let id = { id = prefix op; id_loc = loc_i 1 } in
let id = { id = prefix op; id_lab = []; id_loc = loc_i 1 } in
mk_expr (mk_apply_id id [e1])
let id_unit () = { id = "unit"; id_loc = loc () }
let id_result () = { id = "result"; id_loc = loc () }
let id_anonymous () = { id = "_"; id_loc = loc () }
let exit_exn () = { id = "%Exit"; id_loc = loc () }
let id_unit () = { id = "unit"; id_lab = []; id_loc = loc () }
let id_result () = { id = "result"; id_lab = []; id_loc = loc () }
let id_anonymous () = { id = "_"; id_lab = []; id_loc = loc () }
let exit_exn () = { id = "%Exit"; id_lab = []; id_loc = loc () }
let id_lt_nat () = Qident { id = "lt_nat"; id_loc = loc () }
let id_lt_nat () = Qident { id = "lt_nat"; id_lab = []; id_loc = loc () }
let ty_unit () = Tpure (PPTtyapp ([], Qident (id_unit ())))
......@@ -116,7 +127,7 @@
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON
%token COLONEQUAL ARROW EQUAL LTGT AT DOT LEFTSQ RIGHTSQ
%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP
%token LEFTPAR_STAR_RIGHTPAR EOF
%token BACKQUOTE LEFTPAR_STAR_RIGHTPAR EOF
/* Precedences */
......@@ -187,18 +198,18 @@ list1_decl:
decl:
| LOGIC
{ Dlogic $1 }
| LET lident list1_type_v_binder opt_cast EQUAL triple
{ Dlet ($2, mk_expr_i 3 (Efun ($3, cast_body $4 $6))) }
| LET lident EQUAL FUN list1_type_v_binder ARROW triple
{ Dlet ($2, mk_expr_i 3 (Efun ($5, $7))) }
| LET lident labels list1_type_v_binder opt_cast EQUAL triple
{ Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
| LET lident labels EQUAL FUN list1_type_v_binder ARROW triple
{ Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
| PARAMETER lident COLON type_v
{ Dparam ($2, $4) }
| EXCEPTION uident
{ Dexn ($2, None) }
| EXCEPTION uident OF pure_type
{ Dexn ($2, Some $4) }
| PARAMETER lident labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, None) }
| EXCEPTION uident labels OF pure_type
{ Dexn (add_lab $2 $3, Some $5) }
;
list1_recfun_sep_and:
......@@ -207,16 +218,16 @@ list1_recfun_sep_and:
;
recfun:
| lident list1_type_v_binder opt_cast opt_variant EQUAL triple
{ $1, $2, $4, cast_body $3 $6 }
| lident labels list1_type_v_binder opt_cast opt_variant EQUAL triple
{ add_lab $1 $2, $3, $5, cast_body $4 $7 }
;
lident:
| LIDENT { { id = $1; id_loc = loc () } }
| LIDENT { { id = $1; id_lab = []; id_loc = loc () } }
;
uident:
| UIDENT { { id = $1; id_loc = loc () } }
| UIDENT { { id = $1; id_lab = []; id_loc = loc () } }
;
ident:
......@@ -253,7 +264,7 @@ expr:
{ mk_infix $1 "=" $3 }
| expr LTGT expr
{ let t = mk_infix $1 "=" $3 in
mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [t]) }
mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = loc () } [t]) }
| expr OP1 expr
{ mk_infix $1 $2 $3 }
| expr OP2 expr
......@@ -263,7 +274,7 @@ expr:
| expr OP4 expr
{ mk_infix $1 $2 $3 }
| NOT expr %prec prefix_op
{ mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [$2]) }
{ mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = loc () } [$2]) }
| any_op expr %prec prefix_op
{ mk_prefix $1 $2 }
| expr COLONEQUAL expr
......@@ -286,8 +297,8 @@ expr:
{ match $2.pat_desc with
| PPpvar id -> mk_expr (Elet (id, $4, $6))
| _ -> mk_expr (Ematch ($4, [$2, $6])) }
| LET lident list1_type_v_binder EQUAL triple IN expr
{ mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, $5)), $7)) }
| LET lident labels list1_type_v_binder EQUAL triple IN expr
{ mk_expr (Elet (add_lab $2 $3, mk_expr_i 6 (Efun ($4, $6)), $8)) }
| LET REC list1_recfun_sep_and IN expr
{ mk_expr (Eletrec ($3, $5)) }
| FUN list1_type_v_binder ARROW triple
......@@ -399,7 +410,7 @@ list1_pat_uni:
pat_uni:
| pat_arg { $1 }
| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident { mk_pat (PPpas ($1, $3)) }
| pat_uni AS lident labels { mk_pat (PPpas ($1, add_lab $3 $4)) }
;
list1_pat_arg:
......@@ -409,11 +420,9 @@ list1_pat_arg:
pat_arg:
| UNDERSCORE { mk_pat (PPpwild) }
| lident { mk_pat (PPpvar $1) }
| lident labels { mk_pat (PPpvar (add_lab $1 $2)) }
| uqualid { mk_pat (PPpapp ($1, [])) }
/*
| LEFTPAR RIGHTPAR { mk_pat (PPptuple []) }
*/
| LEFTPAR pattern RIGHTPAR { $2 }
;
......@@ -465,10 +474,8 @@ pure_type_arg_no_paren:
{ PPTtyapp ([], $1) }
| LEFTPAR pure_type COMMA list1_pure_type_sep_comma RIGHTPAR
{ PPTtuple ($2 :: $4) }
/*
| LEFTPAR RIGHTPAR
{ PPTtuple ([]) }
*/
;
list1_pure_type_sep_comma:
......@@ -482,17 +489,17 @@ list1_type_v_binder:
;
type_v_binder:
| lident
{ [$1, None] }
| lident labels
{ [add_lab $1 $2, None] }
| LEFTPAR RIGHTPAR
{ [id_anonymous (), Some (ty_unit ())] }
| LEFTPAR lidents COLON type_v RIGHTPAR
| LEFTPAR lidents_lab COLON type_v RIGHTPAR
{ List.map (fun i -> (i, Some $4)) $2 }
;
lidents:
| lident { [$1] }
| lident lidents { $1 :: $2 }
lidents_lab:
| lident labels { add_lab $1 $2 :: [] }
| lident labels lidents_lab { add_lab $1 $2 :: $3 }
;
type_v:
......@@ -500,8 +507,8 @@ type_v:
{ $1 }
| simple_type_v ARROW type_c
{ Tarrow ([id_anonymous (), Some $1], $3) }
| lident COLON simple_type_v ARROW type_c
{ Tarrow ([$1, Some $3], $5) }
| lident labels COLON simple_type_v ARROW type_c
{ Tarrow ([add_lab $1 $2, Some $4], $6) }
/* TODO: we could alllow lidents instead, e.g. x y : int -> ... */
/*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
;
......@@ -603,6 +610,21 @@ list1_uident_sep_comma:
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
;
label:
| STRING
{ Ident.label $1 }
| STRING BACKQUOTE INTEGER BACKQUOTE INTEGER
BACKQUOTE INTEGER BACKQUOTE INTEGER BACKQUOTE STRING
{ let loc = user_loc $11 (int_of_string $3) (int_of_string $5)
(int_of_string $7) (int_of_string $9) in
Ident.label ~loc $1 }
;
labels:
| /* epsilon */ { [] }
| label labels { $1 :: $2 }
;
/*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
......
......@@ -117,7 +117,9 @@ and specialize_type_c ~loc htv c =
dc_post = specialize_post ~loc htv c.c_post; }
and specialize_binder ~loc htv (vs, tyv) =
let id = { id = vs.vs_name.id_string; id_loc = loc } in
let id = { id = vs.vs_name.id_string;
id_lab = vs.vs_name.id_label;
id_loc = loc } in
id, specialize_type_v ~loc htv tyv
let specialize_global loc x gl =
......
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