Refactoring of the parser and AST so "let" constructs bind
exactly one variable. (Unfinished) Fixed minor error in error printing in Lexer. Added test in ParseMain.ml on --verbose=parser.
This commit is contained in:
parent
331b11dcca
commit
24a1068dd4
@ -116,7 +116,7 @@ and declaration =
|
|||||||
(* Non-recursive values *)
|
(* Non-recursive values *)
|
||||||
|
|
||||||
and let_binding = {
|
and let_binding = {
|
||||||
pattern : pattern;
|
variable : variable;
|
||||||
lhs_type : (colon * type_expr) option;
|
lhs_type : (colon * type_expr) option;
|
||||||
eq : equal;
|
eq : equal;
|
||||||
let_rhs : expr
|
let_rhs : expr
|
||||||
@ -320,11 +320,18 @@ and 'a case_clause = {
|
|||||||
|
|
||||||
and let_in = {
|
and let_in = {
|
||||||
kwd_let : kwd_let;
|
kwd_let : kwd_let;
|
||||||
binding : let_binding;
|
binding : let_in_binding;
|
||||||
kwd_in : kwd_in;
|
kwd_in : kwd_in;
|
||||||
body : expr
|
body : expr
|
||||||
}
|
}
|
||||||
|
|
||||||
|
and let_in_binding = {
|
||||||
|
pattern : pattern;
|
||||||
|
lhs_type : (colon * type_expr) option;
|
||||||
|
eq : equal;
|
||||||
|
let_rhs : expr
|
||||||
|
}
|
||||||
|
|
||||||
and fun_expr = {
|
and fun_expr = {
|
||||||
kwd_fun : kwd_fun;
|
kwd_fun : kwd_fun;
|
||||||
param : variable;
|
param : variable;
|
||||||
@ -345,16 +352,27 @@ and conditional = {
|
|||||||
|
|
||||||
let sprintf = Printf.sprintf
|
let sprintf = Printf.sprintf
|
||||||
|
|
||||||
|
let region_of_type_expr = function
|
||||||
|
TProd {region; _}
|
||||||
|
| TSum {region; _}
|
||||||
|
| TRecord {region; _}
|
||||||
|
| TApp {region; _}
|
||||||
|
| TFun {region; _}
|
||||||
|
| TPar {region; _}
|
||||||
|
| TAlias {region; _} -> region
|
||||||
|
|
||||||
|
|
||||||
let region_of_list_pattern = function
|
let region_of_list_pattern = function
|
||||||
Sugar {region; _} | PCons {region; _} -> region
|
Sugar {region; _} | PCons {region; _} -> region
|
||||||
|
|
||||||
let region_of_pattern = function
|
let region_of_pattern = function
|
||||||
PList p -> region_of_list_pattern p
|
PList p -> region_of_list_pattern p
|
||||||
| PTuple {region;_} | PVar {region;_}
|
| PTuple {region;_} | PVar {region;_}
|
||||||
| PUnit {region;_} | PInt {region;_} | PTrue region | PFalse region
|
| PUnit {region;_} | PInt {region;_}
|
||||||
|
| PTrue region | PFalse region
|
||||||
| PString {region;_} | PWild region
|
| PString {region;_} | PWild region
|
||||||
| PConstr {region; _} | PPar {region;_} | PRecord {region; _}
|
| PConstr {region; _} | PPar {region;_}
|
||||||
| PTyped {region; _} -> region
|
| PRecord {region; _} | PTyped {region; _} -> region
|
||||||
|
|
||||||
let region_of_bool_expr = function
|
let region_of_bool_expr = function
|
||||||
Or {region;_} | And {region;_}
|
Or {region;_} | And {region;_}
|
||||||
@ -472,9 +490,9 @@ and print_type_par {value={lpar;inside=t;rpar}; _} =
|
|||||||
print_type_expr t;
|
print_type_expr t;
|
||||||
print_token rpar ")"
|
print_token rpar ")"
|
||||||
|
|
||||||
and print_projection Region.{value; _} =
|
and print_projection node =
|
||||||
let {struct_name; selector; field_path} = value in
|
let {struct_name; selector; field_path} = node in
|
||||||
print_uident struct_name;
|
print_var struct_name;
|
||||||
print_token selector ".";
|
print_token selector ".";
|
||||||
print_nsepseq "." print_selection field_path
|
print_nsepseq "." print_selection field_path
|
||||||
|
|
||||||
@ -532,7 +550,17 @@ and print_terminator = function
|
|||||||
Some semi -> print_token semi ";"
|
Some semi -> print_token semi ";"
|
||||||
| None -> ()
|
| None -> ()
|
||||||
|
|
||||||
and print_let_binding {pattern; lhs_type; eq; let_rhs} =
|
and print_let_binding {variable; lhs_type; eq; let_rhs} =
|
||||||
|
print_var variable;
|
||||||
|
(match lhs_type with
|
||||||
|
None -> ()
|
||||||
|
| Some (colon, type_expr) ->
|
||||||
|
print_token colon ":";
|
||||||
|
print_type_expr type_expr);
|
||||||
|
(print_token eq "="; print_expr let_rhs)
|
||||||
|
|
||||||
|
and print_let_in_binding (bind: let_in_binding) =
|
||||||
|
let {pattern; lhs_type; eq; let_rhs} : let_in_binding = bind in
|
||||||
print_pattern pattern;
|
print_pattern pattern;
|
||||||
(match lhs_type with
|
(match lhs_type with
|
||||||
None -> ()
|
None -> ()
|
||||||
@ -603,7 +631,7 @@ and print_expr = function
|
|||||||
| ECall {value=f,l; _} ->
|
| ECall {value=f,l; _} ->
|
||||||
print_expr f; Utils.nseq_iter print_expr l
|
print_expr f; Utils.nseq_iter print_expr l
|
||||||
| EVar v -> print_var v
|
| EVar v -> print_var v
|
||||||
| EProj p -> print_projection p
|
| EProj p -> print_projection p.value
|
||||||
| EUnit {value=lpar,rpar; _} ->
|
| EUnit {value=lpar,rpar; _} ->
|
||||||
print_token lpar "("; print_token rpar ")"
|
print_token lpar "("; print_token rpar ")"
|
||||||
| EBytes b -> print_bytes b
|
| EBytes b -> print_bytes b
|
||||||
@ -717,9 +745,10 @@ and print_case_clause {value; _} =
|
|||||||
print_token arrow "->";
|
print_token arrow "->";
|
||||||
print_expr rhs
|
print_expr rhs
|
||||||
|
|
||||||
and print_let_in {kwd_let; binding; kwd_in; body} =
|
and print_let_in (bind: let_in) =
|
||||||
|
let {kwd_let; binding; kwd_in; body} = bind in
|
||||||
print_token kwd_let "let";
|
print_token kwd_let "let";
|
||||||
print_let_binding binding;
|
print_let_in_binding binding;
|
||||||
print_token kwd_in "in";
|
print_token kwd_in "in";
|
||||||
print_expr body
|
print_expr body
|
||||||
|
|
||||||
|
@ -118,14 +118,14 @@ and ast = t
|
|||||||
and eof = Region.t
|
and eof = Region.t
|
||||||
|
|
||||||
and declaration =
|
and declaration =
|
||||||
Let of (kwd_let * let_binding) reg (* let p = e *)
|
Let of (kwd_let * let_binding) reg (* let x = e *)
|
||||||
| LetEntry of (kwd_let_entry * let_binding) reg (* let%entry p = e *)
|
| LetEntry of (kwd_let_entry * let_binding) reg (* let%entry x = e *)
|
||||||
| TypeDecl of type_decl reg (* type ... *)
|
| TypeDecl of type_decl reg (* type ... *)
|
||||||
|
|
||||||
(* Non-recursive values *)
|
(* Non-recursive values *)
|
||||||
|
|
||||||
and let_binding = { (* p = e p : t = e *)
|
and let_binding = { (* p = e p : t = e *)
|
||||||
pattern : pattern;
|
variable : variable;
|
||||||
lhs_type : (colon * type_expr) option;
|
lhs_type : (colon * type_expr) option;
|
||||||
eq : equal;
|
eq : equal;
|
||||||
let_rhs : expr
|
let_rhs : expr
|
||||||
@ -329,11 +329,18 @@ and 'a case_clause = {
|
|||||||
|
|
||||||
and let_in = {
|
and let_in = {
|
||||||
kwd_let : kwd_let;
|
kwd_let : kwd_let;
|
||||||
binding : let_binding;
|
binding : let_in_binding;
|
||||||
kwd_in : kwd_in;
|
kwd_in : kwd_in;
|
||||||
body : expr
|
body : expr
|
||||||
}
|
}
|
||||||
|
|
||||||
|
and let_in_binding = {
|
||||||
|
pattern : pattern;
|
||||||
|
lhs_type : (colon * type_expr) option;
|
||||||
|
eq : equal;
|
||||||
|
let_rhs : expr
|
||||||
|
}
|
||||||
|
|
||||||
and fun_expr = {
|
and fun_expr = {
|
||||||
kwd_fun : kwd_fun;
|
kwd_fun : kwd_fun;
|
||||||
param : variable;
|
param : variable;
|
||||||
@ -471,6 +478,7 @@ val print_tokens : (*?undo:bool ->*) ast -> unit
|
|||||||
|
|
||||||
val region_of_pattern : pattern -> Region.t
|
val region_of_pattern : pattern -> Region.t
|
||||||
val region_of_expr : expr -> Region.t
|
val region_of_expr : expr -> Region.t
|
||||||
|
val region_of_type_expr : type_expr -> Region.t
|
||||||
|
|
||||||
(* Simplifications *)
|
(* Simplifications *)
|
||||||
|
|
||||||
@ -479,3 +487,7 @@ val region_of_expr : expr -> Region.t
|
|||||||
contains. *)
|
contains. *)
|
||||||
|
|
||||||
val unpar : expr -> expr
|
val unpar : expr -> expr
|
||||||
|
|
||||||
|
(* TODO *)
|
||||||
|
|
||||||
|
val print_projection : projection -> unit
|
||||||
|
@ -27,8 +27,7 @@ let help () =
|
|||||||
print_endline " (default: <input>.ml)";
|
print_endline " (default: <input>.ml)";
|
||||||
print_endline " -e, --eval Interpret <input>.mml or stdin";
|
print_endline " -e, --eval Interpret <input>.mml or stdin";
|
||||||
print_endline " --raw-edits Do not optimise translation edits";
|
print_endline " --raw-edits Do not optimise translation edits";
|
||||||
print_endline " --verbose=<phases> Colon-separated phases: cmdline, lexer,";
|
print_endline " --verbose=<phases> Colon-separated phases: cmdline, lexer, parser";
|
||||||
print_endline " parser, unparsing, norm, eval";
|
|
||||||
print_endline " --version Short commit hash on stdout";
|
print_endline " --version Short commit hash on stdout";
|
||||||
print_endline " -h, --help This help";
|
print_endline " -h, --help This help";
|
||||||
exit 0
|
exit 0
|
||||||
|
@ -414,7 +414,7 @@ let get_token ?log =
|
|||||||
(* TODO: Move out (functor). See LIGO. *)
|
(* TODO: Move out (functor). See LIGO. *)
|
||||||
|
|
||||||
let format_error ~(kind: string) Region.{region; value=msg} =
|
let format_error ~(kind: string) Region.{region; value=msg} =
|
||||||
sprintf "%s error in %s:\n%s%!"
|
sprintf "%s error %s:\n%s%!"
|
||||||
kind (region#to_string `Byte) msg
|
kind (region#to_string `Byte) msg
|
||||||
|
|
||||||
let prerr ~(kind: string) msg =
|
let prerr ~(kind: string) msg =
|
||||||
|
@ -3,11 +3,104 @@
|
|||||||
|
|
||||||
open AST
|
open AST
|
||||||
|
|
||||||
|
(* Rewrite "let pattern = e" as "let x = e;; let x1 = ...;; let x2 = ...;;" *)
|
||||||
|
|
||||||
|
module VMap = Utils.String.Map
|
||||||
|
|
||||||
|
let ghost_of value = Region.{region=ghost; value}
|
||||||
|
let ghost = Region.ghost
|
||||||
|
|
||||||
|
let mk_component rank =
|
||||||
|
let num = string_of_int rank, Z.of_int rank in
|
||||||
|
let par = {lpar=ghost; inside = ghost_of num; rpar=ghost}
|
||||||
|
in Component (ghost_of par)
|
||||||
|
|
||||||
|
let rec mk_field_path (rank, tail) =
|
||||||
|
let head = mk_component rank in
|
||||||
|
match tail with
|
||||||
|
[] -> head, []
|
||||||
|
| hd::tl -> mk_field_path (hd,tl) |> Utils.nsepseq_cons head ghost
|
||||||
|
|
||||||
|
let mk_projection (fresh : variable) (path : int Utils.nseq) =
|
||||||
|
{struct_name = fresh;
|
||||||
|
selector = ghost;
|
||||||
|
field_path = Utils.nsepseq_rev (mk_field_path path)}
|
||||||
|
|
||||||
|
let rec sub_rec fresh path (map, rank) pattern =
|
||||||
|
let path' = Utils.nseq_cons rank path in
|
||||||
|
let map' = split fresh map path' pattern
|
||||||
|
in map', rank+1
|
||||||
|
|
||||||
|
and split fresh map path = function
|
||||||
|
PTuple t -> let apply = sub_rec fresh path in
|
||||||
|
Utils.nsepseq_foldl apply (map,1) t.value |> fst
|
||||||
|
| PPar p -> split fresh map path p.value.inside
|
||||||
|
| PVar v -> if VMap.mem v.value map
|
||||||
|
then let err = Region.{value="Non-linear pattern.";
|
||||||
|
region=v.region}
|
||||||
|
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
||||||
|
else VMap.add v.value (mk_projection fresh path) map
|
||||||
|
| PWild _ -> map
|
||||||
|
| PUnit _ -> map (* TODO *)
|
||||||
|
| PConstr {region; _}
|
||||||
|
| PTyped {region; _} ->
|
||||||
|
let err = Region.{value="Not implemented yet."; region}
|
||||||
|
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
||||||
|
| _ -> assert false
|
||||||
|
|
||||||
|
let rec split_pattern = function
|
||||||
|
PPar p -> split_pattern p.value.inside
|
||||||
|
| PTyped {value=p; _} ->
|
||||||
|
let var', type', map = split_pattern p.pattern in
|
||||||
|
(match type' with
|
||||||
|
None -> var', Some p.type_expr, map
|
||||||
|
| Some t when t = p.type_expr -> var', Some t, map (* hack *)
|
||||||
|
| Some t ->
|
||||||
|
let reg = AST.region_of_type_expr t in
|
||||||
|
let reg = reg#to_string `Byte in
|
||||||
|
let value =
|
||||||
|
Printf.sprintf "Unification with %s is not\
|
||||||
|
implemented." reg in
|
||||||
|
let region = AST.region_of_type_expr p.type_expr in
|
||||||
|
let err = Region.{value; region} in
|
||||||
|
(Lexer.prerr ~kind:"Syntactical" err; exit 1))
|
||||||
|
| PConstr {region; _} (* TODO *)
|
||||||
|
| PRecord {region; _} ->
|
||||||
|
let err = Region.{value="Not implemented yet."; region}
|
||||||
|
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
||||||
|
| PUnit _ ->
|
||||||
|
let fresh = Utils.gen_sym () |> ghost_of in
|
||||||
|
let unit = TAlias (ghost_of "unit")
|
||||||
|
in fresh, Some unit, VMap.empty
|
||||||
|
| PVar v -> v, None, VMap.empty
|
||||||
|
| PWild _ -> Utils.gen_sym () |> ghost_of, None, VMap.empty
|
||||||
|
| PInt {region;_} | PTrue region
|
||||||
|
| PFalse region | PString {region;_}
|
||||||
|
| PList Sugar {region; _} | PList PCons {region; _} ->
|
||||||
|
let err = Region.{value="Incomplete pattern."; region}
|
||||||
|
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
||||||
|
| PTuple t ->
|
||||||
|
let fresh = Utils.gen_sym () |> ghost_of
|
||||||
|
and init = VMap.empty, 1 in
|
||||||
|
let apply (map, rank) pattern =
|
||||||
|
split fresh map (rank,[]) pattern, rank+1 in
|
||||||
|
let map = Utils.nsepseq_foldl apply init t.value |> fst
|
||||||
|
in fresh, None, map
|
||||||
|
|
||||||
|
let mk_let_bindings =
|
||||||
|
let apply var proj let_bindings =
|
||||||
|
let new_bind : let_binding = {
|
||||||
|
variable = ghost_of var;
|
||||||
|
lhs_type = None;
|
||||||
|
eq = ghost;
|
||||||
|
let_rhs = EProj (ghost_of proj)} in
|
||||||
|
let new_let = Let (ghost_of (ghost, new_bind))
|
||||||
|
in Utils.nseq_cons new_let let_bindings
|
||||||
|
in VMap.fold apply
|
||||||
|
|
||||||
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
||||||
|
|
||||||
let norm_fun_expr patterns expr =
|
let norm_fun_expr patterns expr =
|
||||||
let ghost_of value = Region.{region=ghost; value} in
|
|
||||||
let ghost = Region.ghost in
|
|
||||||
let apply pattern expr =
|
let apply pattern expr =
|
||||||
match pattern with
|
match pattern with
|
||||||
PVar var ->
|
PVar var ->
|
||||||
@ -15,8 +108,8 @@ let norm_fun_expr patterns expr =
|
|||||||
kwd_fun = ghost;
|
kwd_fun = ghost;
|
||||||
param = var;
|
param = var;
|
||||||
arrow = ghost;
|
arrow = ghost;
|
||||||
body = expr} in
|
body = expr}
|
||||||
EFun (ghost_of fun_expr)
|
in EFun (ghost_of fun_expr)
|
||||||
| _ -> let fresh = Utils.gen_sym () |> ghost_of in
|
| _ -> let fresh = Utils.gen_sym () |> ghost_of in
|
||||||
let clause = {pattern; arrow=ghost; rhs=expr} in
|
let clause = {pattern; arrow=ghost; rhs=expr} in
|
||||||
let clause = ghost_of clause in
|
let clause = ghost_of clause in
|
||||||
@ -37,17 +130,6 @@ let norm_fun_expr patterns expr =
|
|||||||
in EFun (ghost_of fun_expr)
|
in EFun (ghost_of fun_expr)
|
||||||
in Utils.nseq_foldr apply patterns expr
|
in Utils.nseq_foldr apply patterns expr
|
||||||
|
|
||||||
(*
|
|
||||||
let norm_fun_expr patterns expr =
|
|
||||||
let apply pattern expr =
|
|
||||||
let fun_expr = {
|
|
||||||
kwd_fun = Region.ghost;
|
|
||||||
param = pattern;
|
|
||||||
arrow = Region.ghost;
|
|
||||||
body = expr} in
|
|
||||||
EFun {region=Region.ghost; value=fun_expr}
|
|
||||||
in Utils.nseq_foldr apply patterns expr
|
|
||||||
*)
|
|
||||||
(* END HEADER *)
|
(* END HEADER *)
|
||||||
%}
|
%}
|
||||||
|
|
||||||
@ -172,7 +254,7 @@ sepseq(item,sep):
|
|||||||
type_name : ident { $1 }
|
type_name : ident { $1 }
|
||||||
field_name : ident { $1 }
|
field_name : ident { $1 }
|
||||||
module_name : constr { $1 }
|
module_name : constr { $1 }
|
||||||
struct_name : Ident { $1 }
|
struct_name : ident { $1 }
|
||||||
|
|
||||||
(* Non-empty comma-separated values (at least two values) *)
|
(* Non-empty comma-separated values (at least two values) *)
|
||||||
|
|
||||||
@ -191,12 +273,17 @@ list_of(item):
|
|||||||
(* Main *)
|
(* Main *)
|
||||||
|
|
||||||
program:
|
program:
|
||||||
nseq(declaration) eof { {decl=$1; eof=$2} }
|
declarations eof { {decl = Utils.nseq_rev $1; eof=$2} }
|
||||||
|
|
||||||
|
declarations:
|
||||||
|
declaration { $1 }
|
||||||
|
| declaration declarations {
|
||||||
|
Utils.(nseq_foldl (fun x y -> nseq_cons y x) $2 $1) }
|
||||||
|
|
||||||
declaration:
|
declaration:
|
||||||
reg(kwd(Let) let_binding {$1,$2}) { Let $1 }
|
reg(kwd(LetEntry) entry_binding {$1,$2}) { LetEntry $1, [] }
|
||||||
| reg(kwd(LetEntry) let_binding {$1,$2}) { LetEntry $1 }
|
| reg(type_decl) { TypeDecl $1, [] }
|
||||||
| reg(type_decl) { TypeDecl $1 }
|
| let_declaration { $1 }
|
||||||
|
|
||||||
(* Type declarations *)
|
(* Type declarations *)
|
||||||
|
|
||||||
@ -227,8 +314,8 @@ core_type:
|
|||||||
let arg, constr = $1.value in
|
let arg, constr = $1.value in
|
||||||
let Region.{value=arg_val; _} = arg in
|
let Region.{value=arg_val; _} = arg in
|
||||||
let lpar, rpar = Region.ghost, Region.ghost in
|
let lpar, rpar = Region.ghost, Region.ghost in
|
||||||
let arg_val = {lpar; inside=arg_val,[]; rpar} in
|
let value = {lpar; inside=arg_val,[]; rpar} in
|
||||||
let arg = {arg with value=arg_val} in
|
let arg = {arg with value} in
|
||||||
TApp Region.{$1 with value = constr, arg}
|
TApp Region.{$1 with value = constr, arg}
|
||||||
}
|
}
|
||||||
| reg(type_tuple type_constr {$1,$2}) {
|
| reg(type_tuple type_constr {$1,$2}) {
|
||||||
@ -236,8 +323,8 @@ core_type:
|
|||||||
TApp Region.{$1 with value = constr, arg}
|
TApp Region.{$1 with value = constr, arg}
|
||||||
}
|
}
|
||||||
| par(cartesian) {
|
| par(cartesian) {
|
||||||
let Region.{region; value={lpar; inside=prod; rpar}} = $1 in
|
let Region.{value={inside=prod; _}; _} = $1 in
|
||||||
TPar Region.{region; value={lpar; inside = TProd prod; rpar}} }
|
TPar {$1 with value={$1.value with inside = TProd prod}} }
|
||||||
|
|
||||||
type_projection:
|
type_projection:
|
||||||
type_name {
|
type_name {
|
||||||
@ -277,15 +364,46 @@ field_decl:
|
|||||||
field_name colon type_expr {
|
field_name colon type_expr {
|
||||||
{field_name=$1; colon=$2; field_type=$3} }
|
{field_name=$1; colon=$2; field_type=$3} }
|
||||||
|
|
||||||
(* Non-recursive definitions *)
|
(* Entry points *)
|
||||||
|
|
||||||
|
entry_binding:
|
||||||
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
|
let let_rhs = norm_fun_expr $2 $5 in
|
||||||
|
{variable = $1; lhs_type=$3; eq=$4; let_rhs} : let_binding
|
||||||
|
}
|
||||||
|
| ident type_annotation? eq fun_expr(expr) {
|
||||||
|
{variable = $1; lhs_type=$2; eq=$3; let_rhs=$4} : let_binding }
|
||||||
|
|
||||||
|
(* Top-level non-recursive definitions *)
|
||||||
|
|
||||||
|
let_declaration:
|
||||||
|
reg(kwd(Let) let_binding {$1,$2}) {
|
||||||
|
let kwd_let, (binding, map) = $1.value in
|
||||||
|
let let0 = Let {$1 with value = kwd_let, binding}
|
||||||
|
in mk_let_bindings map (let0,[])
|
||||||
|
}
|
||||||
|
|
||||||
let_binding:
|
let_binding:
|
||||||
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
let let_rhs = norm_fun_expr $2 $5 in
|
let let_rhs = norm_fun_expr $2 $5 in
|
||||||
{pattern = PVar $1; lhs_type=$3; eq = Region.ghost; let_rhs}
|
let map = VMap.empty in
|
||||||
|
({variable=$1; lhs_type=$3; eq=$4; let_rhs}: let_binding), map
|
||||||
}
|
}
|
||||||
| irrefutable type_annotation? eq expr {
|
| irrefutable type_annotation? eq expr {
|
||||||
{pattern=$1; lhs_type=$2; eq=$3; let_rhs=$4} }
|
let variable, type_opt, map = split_pattern $1 in
|
||||||
|
({variable; lhs_type=$2; eq=$3; let_rhs=$4}: let_binding), map }
|
||||||
|
|
||||||
|
(* TODO *)
|
||||||
|
|
||||||
|
let_in_binding:
|
||||||
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
|
let let_rhs = norm_fun_expr $2 $5 in
|
||||||
|
{pattern = PVar $1; lhs_type=$3; eq=$4; let_rhs}: let_in_binding
|
||||||
|
}
|
||||||
|
| irrefutable type_annotation? eq expr {
|
||||||
|
let variable, type_opt, map = split_pattern $1 in
|
||||||
|
{pattern = PVar variable; lhs_type=$2; eq=$3; let_rhs=$4}
|
||||||
|
: let_in_binding }
|
||||||
|
|
||||||
type_annotation:
|
type_annotation:
|
||||||
colon type_expr { $1,$2 }
|
colon type_expr { $1,$2 }
|
||||||
@ -303,8 +421,7 @@ sub_irrefutable:
|
|||||||
| par(closed_irrefutable) { PPar $1 }
|
| par(closed_irrefutable) { PPar $1 }
|
||||||
|
|
||||||
closed_irrefutable:
|
closed_irrefutable:
|
||||||
reg(tuple(sub_irrefutable)) { PTuple $1 }
|
irrefutable { $1 }
|
||||||
| sub_irrefutable { $1 }
|
|
||||||
| reg(constr_pattern) { PConstr $1 }
|
| reg(constr_pattern) { PConstr $1 }
|
||||||
| reg(typed_pattern) { PTyped $1 }
|
| reg(typed_pattern) { PTyped $1 }
|
||||||
|
|
||||||
@ -384,11 +501,10 @@ conditional(right_expr):
|
|||||||
|
|
||||||
if_then(right_expr):
|
if_then(right_expr):
|
||||||
kwd(If) expr kwd(Then) right_expr {
|
kwd(If) expr kwd(Then) right_expr {
|
||||||
let open Region in
|
|
||||||
let the_unit = ghost, ghost in
|
let the_unit = ghost, ghost in
|
||||||
let ifnot = EUnit {region=ghost; value=the_unit} in
|
let ifnot = EUnit {region=ghost; value=the_unit} in
|
||||||
{kwd_if=$1; test=$2; kwd_then=$3; ifso=$4;
|
{kwd_if=$1; test=$2; kwd_then=$3; ifso=$4;
|
||||||
kwd_else=Region.ghost; ifnot} }
|
kwd_else=ghost; ifnot} }
|
||||||
|
|
||||||
if_then_else(right_expr):
|
if_then_else(right_expr):
|
||||||
kwd(If) expr kwd(Then) closed_if kwd(Else) right_expr {
|
kwd(If) expr kwd(Then) closed_if kwd(Else) right_expr {
|
||||||
@ -414,13 +530,12 @@ match_expr(right_expr):
|
|||||||
closing = End Region.ghost}
|
closing = End Region.ghost}
|
||||||
}
|
}
|
||||||
| kwd(MatchNat) expr kwd(With) vbar? reg(cases(right_expr)) {
|
| kwd(MatchNat) expr kwd(With) vbar? reg(cases(right_expr)) {
|
||||||
let open Region in
|
|
||||||
let cases = Utils.nsepseq_rev $5.value in
|
let cases = Utils.nsepseq_rev $5.value in
|
||||||
let cast = EVar {region=ghost; value="assert_pos"} in
|
let cast = EVar {region=ghost; value="assert_pos"} in
|
||||||
let cast = ECall {region=ghost; value=cast,($2,[])} in
|
let cast = ECall {region=ghost; value=cast,($2,[])} in
|
||||||
{kwd_match = $1; expr = cast; opening = With $3;
|
{kwd_match = $1; expr = cast; opening = With $3;
|
||||||
lead_vbar = $4; cases = {$5 with value=cases};
|
lead_vbar = $4; cases = {$5 with value=cases};
|
||||||
closing = End Region.ghost} }
|
closing = End ghost} }
|
||||||
|
|
||||||
cases(right_expr):
|
cases(right_expr):
|
||||||
reg(case_clause(right_expr)) { $1, [] }
|
reg(case_clause(right_expr)) { $1, [] }
|
||||||
@ -431,7 +546,7 @@ case_clause(right_expr):
|
|||||||
pattern arrow right_expr { {pattern=$1; arrow=$2; rhs=$3} }
|
pattern arrow right_expr { {pattern=$1; arrow=$2; rhs=$3} }
|
||||||
|
|
||||||
let_expr(right_expr):
|
let_expr(right_expr):
|
||||||
reg(kwd(Let) let_binding kwd(In) right_expr {$1,$2,$3,$4}) {
|
reg(kwd(Let) let_in_binding kwd(In) right_expr {$1,$2,$3,$4}) {
|
||||||
let Region.{region; value = kwd_let, binding, kwd_in, body} = $1 in
|
let Region.{region; value = kwd_let, binding, kwd_in, body} = $1 in
|
||||||
let let_in = {kwd_let; binding; kwd_in; body}
|
let let_in = {kwd_let; binding; kwd_in; body}
|
||||||
in ELetIn {region; value=let_in} }
|
in ELetIn {region; value=let_in} }
|
||||||
@ -576,7 +691,7 @@ module_field:
|
|||||||
module_name dot field_name { $1.value ^ "." ^ $3.value }
|
module_name dot field_name { $1.value ^ "." ^ $3.value }
|
||||||
|
|
||||||
projection:
|
projection:
|
||||||
reg(struct_name) dot nsepseq(selection,dot) {
|
struct_name dot nsepseq(selection,dot) {
|
||||||
{struct_name = $1; selector = $2; field_path = $3}
|
{struct_name = $1; selector = $2; field_path = $3}
|
||||||
}
|
}
|
||||||
| reg(module_name dot field_name {$1,$3})
|
| reg(module_name dot field_name {$1,$3})
|
||||||
|
@ -38,7 +38,8 @@ let tokeniser =
|
|||||||
let () =
|
let () =
|
||||||
try
|
try
|
||||||
let ast = Parser.program tokeniser buffer in
|
let ast = Parser.program tokeniser buffer in
|
||||||
AST.print_tokens ast
|
if Utils.String.Set.mem "parser" options.verbose
|
||||||
|
then AST.print_tokens ast
|
||||||
with
|
with
|
||||||
Lexer.Error diag ->
|
Lexer.Error diag ->
|
||||||
close_in cin; Lexer.prerr ~kind:"Lexical" diag
|
close_in cin; Lexer.prerr ~kind:"Lexical" diag
|
||||||
|
@ -141,7 +141,7 @@ end
|
|||||||
|
|
||||||
let gen_sym =
|
let gen_sym =
|
||||||
let counter = ref 0 in
|
let counter = ref 0 in
|
||||||
fun () -> incr counter; "v" ^ string_of_int !counter
|
fun () -> incr counter; "#" ^ string_of_int !counter
|
||||||
|
|
||||||
(* General tracing function *)
|
(* General tracing function *)
|
||||||
|
|
||||||
|
@ -25,73 +25,73 @@ type ('a,'sep) sepseq = ('a,'sep) nsepseq option
|
|||||||
|
|
||||||
(* Consing *)
|
(* Consing *)
|
||||||
|
|
||||||
val nseq_cons: 'a -> 'a nseq -> 'a nseq
|
val nseq_cons : 'a -> 'a nseq -> 'a nseq
|
||||||
val nsepseq_cons: 'a -> 'sep -> ('a,'sep) nsepseq -> ('a,'sep) nsepseq
|
val nsepseq_cons : 'a -> 'sep -> ('a,'sep) nsepseq -> ('a,'sep) nsepseq
|
||||||
val sepseq_cons: 'a -> 'sep -> ('a,'sep) sepseq -> ('a,'sep) nsepseq
|
val sepseq_cons : 'a -> 'sep -> ('a,'sep) sepseq -> ('a,'sep) nsepseq
|
||||||
|
|
||||||
(* Reversing *)
|
(* Reversing *)
|
||||||
|
|
||||||
val nseq_rev: 'a nseq -> 'a nseq
|
val nseq_rev : 'a nseq -> 'a nseq
|
||||||
val nsepseq_rev: ('a,'sep) nsepseq -> ('a,'sep) nsepseq
|
val nsepseq_rev : ('a,'sep) nsepseq -> ('a,'sep) nsepseq
|
||||||
val sepseq_rev: ('a,'sep) sepseq -> ('a,'sep) sepseq
|
val sepseq_rev : ('a,'sep) sepseq -> ('a,'sep) sepseq
|
||||||
|
|
||||||
(* Rightwards iterators *)
|
(* Rightwards iterators *)
|
||||||
|
|
||||||
val nseq_foldl: ('a -> 'b -> 'a) -> 'a -> 'b nseq -> 'a
|
val nseq_foldl : ('a -> 'b -> 'a) -> 'a -> 'b nseq -> 'a
|
||||||
val nsepseq_foldl: ('a -> 'b -> 'a) -> 'a -> ('b,'c) nsepseq -> 'a
|
val nsepseq_foldl : ('a -> 'b -> 'a) -> 'a -> ('b,'c) nsepseq -> 'a
|
||||||
val sepseq_foldl: ('a -> 'b -> 'a) -> 'a -> ('b,'c) sepseq -> 'a
|
val sepseq_foldl : ('a -> 'b -> 'a) -> 'a -> ('b,'c) sepseq -> 'a
|
||||||
|
|
||||||
val nseq_iter: ('a -> unit) -> 'a nseq -> unit
|
val nseq_iter : ('a -> unit) -> 'a nseq -> unit
|
||||||
val nsepseq_iter: ('a -> unit) -> ('a,'b) nsepseq -> unit
|
val nsepseq_iter : ('a -> unit) -> ('a,'b) nsepseq -> unit
|
||||||
val sepseq_iter: ('a -> unit) -> ('a,'b) sepseq -> unit
|
val sepseq_iter : ('a -> unit) -> ('a,'b) sepseq -> unit
|
||||||
|
|
||||||
(* Leftwards iterators *)
|
(* Leftwards iterators *)
|
||||||
|
|
||||||
val nseq_foldr: ('a -> 'b -> 'b) -> 'a nseq -> 'b -> 'b
|
val nseq_foldr : ('a -> 'b -> 'b) -> 'a nseq -> 'b -> 'b
|
||||||
val nsepseq_foldr: ('a -> 'b -> 'b) -> ('a,'c) nsepseq -> 'b -> 'b
|
val nsepseq_foldr : ('a -> 'b -> 'b) -> ('a,'c) nsepseq -> 'b -> 'b
|
||||||
val sepseq_foldr: ('a -> 'b -> 'b) -> ('a,'c) sepseq -> 'b -> 'b
|
val sepseq_foldr : ('a -> 'b -> 'b) -> ('a,'c) sepseq -> 'b -> 'b
|
||||||
|
|
||||||
(* Conversions to lists *)
|
(* Conversions to lists *)
|
||||||
|
|
||||||
val nseq_to_list: 'a nseq -> 'a list
|
val nseq_to_list : 'a nseq -> 'a list
|
||||||
val nsepseq_to_list: ('a,'b) nsepseq -> 'a list
|
val nsepseq_to_list : ('a,'b) nsepseq -> 'a list
|
||||||
val sepseq_to_list: ('a,'b) sepseq -> 'a list
|
val sepseq_to_list : ('a,'b) sepseq -> 'a list
|
||||||
|
|
||||||
(* Effectful symbol generator *)
|
(* Effectful symbol generator *)
|
||||||
|
|
||||||
val gen_sym: unit -> string
|
val gen_sym : unit -> string
|
||||||
|
|
||||||
(* General tracing function *)
|
(* General tracing function *)
|
||||||
|
|
||||||
val trace: string -> out_channel option -> unit
|
val trace : string -> out_channel option -> unit
|
||||||
|
|
||||||
(* Printing a string in red to standard error *)
|
(* Printing a string in red to standard error *)
|
||||||
|
|
||||||
val highlight: string -> unit
|
val highlight : string -> unit
|
||||||
|
|
||||||
(* Working with optional values *)
|
(* Working with optional values *)
|
||||||
|
|
||||||
module Option:
|
module Option:
|
||||||
sig
|
sig
|
||||||
val apply: ('a -> 'b) -> 'a option -> 'b option
|
val apply : ('a -> 'b) -> 'a option -> 'b option
|
||||||
val rev_apply: ('a -> 'a) option -> 'a -> 'a
|
val rev_apply : ('a -> 'a) option -> 'a -> 'a
|
||||||
val to_string: string option -> string
|
val to_string : string option -> string
|
||||||
end
|
end
|
||||||
|
|
||||||
(* An extension to the standard module [String] *)
|
(* An extension to the standard module [String] *)
|
||||||
|
|
||||||
module String:
|
module String :
|
||||||
sig
|
sig
|
||||||
include module type of String
|
include module type of String
|
||||||
module Map: Map.S with type key = t
|
module Map : Map.S with type key = t
|
||||||
module Set: Set.S with type elt = t
|
module Set : Set.S with type elt = t
|
||||||
end
|
end
|
||||||
|
|
||||||
(* Integer maps *)
|
(* Integer maps *)
|
||||||
|
|
||||||
module Int:
|
module Int :
|
||||||
sig
|
sig
|
||||||
type t = int
|
type t = int
|
||||||
module Map: Map.S with type key = t
|
module Map : Map.S with type key = t
|
||||||
module Set: Set.S with type elt = t
|
module Set : Set.S with type elt = t
|
||||||
end
|
end
|
||||||
|
@ -1 +0,0 @@
|
|||||||
let version = "UNKNOWN"
|
|
Loading…
Reference in New Issue
Block a user