balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fixed the translation of let-in.

Browse Source
This commit is contained in:
Christian Rinderknecht 2019-05-24 19:31:39 +02:00
parent a0936d8eb5
commit 28b84e1e65
5 changed files with 102 additions and 126 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/parser/ligodity/AST.ml
View File

@ -320,18 +320,11 @@ and 'a case_clause = {
and let_in = {
kwd_let : kwd_let;
binding : let_in_binding;
binding : let_binding;
kwd_in : kwd_in;
body : expr
}
and let_in_binding = {
pattern : pattern;
lhs_type : (colon * type_expr) option;
eq : equal;
let_rhs : expr
}
and fun_expr = {
kwd_fun : kwd_fun;
param : variable;
@ -559,16 +552,6 @@ and print_let_binding {variable; lhs_type; eq; let_rhs} =
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;
(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_pattern = function
PTuple {value=patterns;_} -> print_csv print_pattern patterns
| PList p -> print_list_pattern p
@ -748,7 +731,7 @@ and print_case_clause {value; _} =
and print_let_in (bind: let_in) =
let {kwd_let; binding; kwd_in; body} = bind in
print_token kwd_let "let";
print_let_in_binding binding;
print_let_binding binding;
print_token kwd_in "in";
print_expr body

33
src/parser/ligodity/AST.mli
View File

@ -243,24 +243,24 @@ and closing =
| RBracket of rbracket
and list_expr =
Cons of cat bin_op reg (* e1 :: e3 *)
| List of expr injection reg (* [e1; e2; ...] *)
(*| Append of (expr * append * expr) reg *) (* e1 @ e2 *)
Cons of cat bin_op reg (* e1 :: e3 *)
| List of expr injection reg (* [e1; e2; ...] *)
(*| Append of (expr * append * expr) reg *) (* e1 @ e2 *)
and string_expr =
Cat of cat bin_op reg (* e1 ^ e2 *)
| String of string reg (* "foo" *)
and arith_expr =
Add of plus bin_op reg (* e1 + e2 *)
| Sub of minus bin_op reg (* e1 - e2 *)
| Mult of times bin_op reg (* e1 * e2 *)
| Div of slash bin_op reg (* e1 / e2 *)
| Mod of kwd_mod bin_op reg (* e1 mod e2 *)
| Neg of minus un_op reg (* -e *)
| Int of (string * Z.t) reg (* 12345 *)
| Nat of (string * Z.t) reg (* 3p *)
| Mtz of (string * Z.t) reg (* 1.00tz 3tz *)
Add of plus bin_op reg (* e1 + e2 *)
| Sub of minus bin_op reg (* e1 - e2 *)
| Mult of times bin_op reg (* e1 * e2 *)
| Div of slash bin_op reg (* e1 / e2 *)
| Mod of kwd_mod bin_op reg (* e1 mod e2 *)
| Neg of minus un_op reg (* -e *)
| Int of (string * Z.t) reg (* 12345 *)
| Nat of (string * Z.t) reg (* 3p *)
| Mtz of (string * Z.t) reg (* 1.00tz 3tz *)
and logic_expr =
BoolExpr of bool_expr
@ -329,18 +329,11 @@ and 'a case_clause = {
and let_in = {
kwd_let : kwd_let;
binding : let_in_binding;
binding : let_binding;
kwd_in : kwd_in;
body : expr
}
and let_in_binding = {
pattern : pattern;
lhs_type : (colon * type_expr) option;
eq : equal;
let_rhs : expr
}
and fun_expr = {
kwd_fun : kwd_fun;
param : variable;

148
src/parser/ligodity/Parser.mly
View File

@ -10,6 +10,16 @@ module VMap = Utils.String.Map
let ghost_of value = Region.{region=ghost; value}
let ghost = Region.ghost
let fail_syn_unif type1 type2 : 'a =
let reg = AST.region_of_type_expr type1 in
let reg = reg#compact ~file:false `Byte in
let value =
Printf.sprintf "Unification with %s is not\
implemented." reg in
let region = AST.region_of_type_expr type2 in
let err = Region.{value; region} in
(Lexer.prerr ~kind:"Syntactical" err; exit 1)
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}
@ -21,10 +31,11 @@ let rec mk_field_path (rank, tail) =
[] -> 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 mk_projection fresh (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
@ -36,49 +47,38 @@ and split fresh map path = function
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
then
let err =
Region.{value="Non-linear pattern."; region=v.region}
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
else
let proj = mk_projection fresh path
in VMap.add v.value (None, proj) map
| PWild _ -> map
| PUnit _ -> map (* TODO *)
| PUnit _ -> let anon = Utils.gen_sym () in
let unit = ghost, TAlias (ghost_of "unit")
and proj = mk_projection fresh path
in VMap.add anon (Some unit, proj) map
| PRecord {region; _}
| PConstr {region; _}
| PTyped {region; _} ->
let err = Region.{value="Not implemented yet."; region}
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
| _ -> assert false
| p -> let _, _, map = split_pattern p in map
let rec split_pattern = function
PPar p -> split_pattern p.value.inside
and split_pattern = function
PPar p -> split_pattern p.value.inside
| PVar v -> v, None, VMap.empty
| PWild _ -> Utils.gen_sym () |> ghost_of, None, VMap.empty
| PUnit _ -> let fresh = Utils.gen_sym () |> ghost_of in
let unit = TAlias (ghost_of "unit")
in fresh, Some unit, VMap.empty
| 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)
| Some t -> fail_syn_unif t p.type_expr)
| PTuple t ->
let fresh = Utils.gen_sym () |> ghost_of
and init = VMap.empty, 1 in
@ -86,16 +86,40 @@ let rec split_pattern = function
split fresh map (rank,[]) pattern, rank+1 in
let map = Utils.nsepseq_foldl apply init t.value |> fst
in fresh, None, map
| PRecord {region; _}
| PConstr {region; _} ->
let err = Region.{value="Not implemented yet."; region}
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
| 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)
let mk_let_bindings =
let apply var proj let_bindings =
let new_bind : let_binding = {
let apply var (lhs_type, proj) =
let new_bind = {
variable = ghost_of var;
lhs_type = None;
lhs_type;
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 Utils.nseq_cons new_let
in VMap.fold apply
let mk_let_in_bindings =
let apply var (lhs_type, proj) acc =
let binding = {
variable = ghost_of var;
lhs_type;
eq = ghost;
let_rhs = EProj (ghost_of proj)} in
let let_in = {
kwd_let = ghost;
binding;
kwd_in = ghost;
body = acc}
in ELetIn (ghost_of let_in)
in VMap.fold apply
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
@ -277,8 +301,7 @@ program:
declarations:
declaration { $1 }
| declaration declarations {
Utils.(nseq_foldl (fun x y -> nseq_cons y x) $2 $1) }
| declaration declarations { Utils.(nseq_foldl (swap nseq_cons) $2 $1)}
declaration:
reg(kwd(LetEntry) entry_binding {$1,$2}) { LetEntry $1, [] }
@ -313,7 +336,7 @@ core_type:
| reg(reg(core_type) type_constr {$1,$2}) {
let arg, constr = $1.value in
let Region.{value=arg_val; _} = arg in
let lpar, rpar = Region.ghost, Region.ghost in
let lpar, rpar = ghost, ghost in
let value = {lpar; inside=arg_val,[]; rpar} in
let arg = {arg with value} in
TApp Region.{$1 with value = constr, arg}
@ -350,7 +373,7 @@ sum_type:
variant:
constr kwd(Of) cartesian { {constr=$1; args = Some ($2,$3)} }
| constr { {constr=$1; args = None} }
| constr { {constr=$1; args = None} }
record_type:
lbrace sep_or_term_list(reg(field_decl),semi) rbrace {
@ -369,10 +392,10 @@ field_decl:
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
{variable = $1; lhs_type=$3; eq=$4; let_rhs}
}
| ident type_annotation? eq fun_expr(expr) {
{variable = $1; lhs_type=$2; eq=$3; let_rhs=$4} : let_binding }
{variable = $1; lhs_type=$2; eq=$3; let_rhs=$4} }
(* Top-level non-recursive definitions *)
@ -387,23 +410,18 @@ let_binding:
ident nseq(sub_irrefutable) type_annotation? eq expr {
let let_rhs = norm_fun_expr $2 $5 in
let map = VMap.empty in
({variable=$1; lhs_type=$3; eq=$4; let_rhs}: let_binding), map
{variable=$1; lhs_type=$3; eq=$4; let_rhs}, map
}
| irrefutable type_annotation? eq expr {
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
let variable, type_opt, map = split_pattern $1 in
match type_opt, $2 with
Some type1, Some (_,type2) when type1 <> type2 ->
fail_syn_unif type1 type2
| Some type1, None ->
let lhs_type = Some (ghost, type1) in
{variable; lhs_type; eq=$3; let_rhs=$4}, map
| _ -> {variable; lhs_type=$2; eq=$3; let_rhs=$4}, map
}
| 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:
colon type_expr { $1,$2 }
@ -418,6 +436,7 @@ sub_irrefutable:
ident { PVar $1 }
| wild { PWild $1 }
| unit { PUnit $1 }
| reg(record_pattern) { PRecord $1 }
| par(closed_irrefutable) { PPar $1 }
closed_irrefutable:
@ -527,7 +546,7 @@ match_expr(right_expr):
let cases = Utils.nsepseq_rev $5.value in
{kwd_match = $1; expr = $2; opening = With $3;
lead_vbar = $4; cases = {$5 with value=cases};
closing = End Region.ghost}
closing = End ghost}
}
| kwd(MatchNat) expr kwd(With) vbar? reg(cases(right_expr)) {
let cases = Utils.nsepseq_rev $5.value in
@ -546,10 +565,11 @@ case_clause(right_expr):
pattern arrow right_expr { {pattern=$1; arrow=$2; rhs=$3} }
let_expr(right_expr):
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
reg(kwd(Let) let_binding kwd(In) right_expr {$1,$2,$3,$4}) {
let kwd_let, (binding, map), kwd_in, body = $1.value in
let body = mk_let_in_bindings map body in
let let_in = {kwd_let; binding; kwd_in; body}
in ELetIn {region; value=let_in} }
in ELetIn {region=$1.region; value=let_in} }
fun_expr(right_expr):
kwd(Fun) nseq(irrefutable) arrow right_expr { norm_fun_expr $2 $4 }

24
src/simplify/ligodity.ml
View File

@ -103,16 +103,13 @@ let rec simpl_expression :
match t with
| Raw.ELetIn e -> (
let Raw.{binding; body; _} = e.value in
let Raw.{pattern; lhs_type; let_rhs; _} = binding in
let Raw.{variable; lhs_type; let_rhs; _} = binding in
let%bind type_annotation = bind_map_option
(fun (_,type_expr) -> simpl_type_expression type_expr)
lhs_type in
let%bind rhs = simpl_expression ?te_annot:type_annotation let_rhs in
let%bind body = simpl_expression body in
match pattern with
Raw.PVar v -> return (mk_let_in (v.value , None) rhs body)
| _ -> let%bind case = simpl_cases [(pattern, body)]
in return (E_matching (rhs, case))
return (mk_let_in (variable.value , None) rhs body)
)
| Raw.EAnnot a -> (
let (expr , type_expr) = a.value in
@ -288,23 +285,6 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
ok @@ loc x @@ (Declaration_constant (name , type_annotation , rhs))
)
(*
| ConstDecl x ->
let simpl_const_decl = fun {name;const_type;init} ->
let%bind expression = simpl_expression init in
let%bind t = simpl_type_expression const_type in
let type_annotation = Some t in
ok @@ Declaration_constant {name=name.value;expression={expression with type_annotation}}
in
bind_map_location simpl_const_decl (Location.lift_region x)
| LambdaDecl (FunDecl x) ->
let aux f x =
let%bind x' = f x in
ok @@ Declaration_constant x' in
bind_map_location (aux simpl_fun_declaration) (Location.lift_region x)
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
*)
and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
let open Raw in
let get_var (t:Raw.pattern) = match t with

2
vendors/ligo-utils vendored

@ -1 +1 @@
Subproject commit c1f0743cb0943d7a5318177d6386122e23711c7e
Subproject commit 533c801c103627484af042bf1f976eeffcf592e3