diff --git a/src/parser/dune b/src/parser/dune
index e08c2915a..eb7dca130 100644
--- a/src/parser/dune
+++ b/src/parser/dune
@@ -6,7 +6,7 @@
tezos-utils
parser_pascaligo
parser_camligo
-;; parser_ligodity
+ parser_ligodity
)
(preprocess
(pps simple-utils.ppx_let_generalized)
diff --git a/src/parser/ligodity/.links b/src/parser/ligodity/.links
index 34a1424ad..8af33d655 100644
--- a/src/parser/ligodity/.links
+++ b/src/parser/ligodity/.links
@@ -1,7 +1,7 @@
$HOME/git/OCaml-build/Makefile
$HOME/git/OCaml-build/Makefile.cfg
-$HOME/git/tezos/src/lib_utils/pos.mli
-$HOME/git/tezos/src/lib_utils/pos.ml
-$HOME/git/tezos/src/lib_utils/region.mli
-$HOME/git/tezos/src/lib_utils/region.ml
-Stubs/Tezos_utils.ml
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.mli
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.ml
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.mli
+$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.ml
+Stubs/Simple_utils.ml
diff --git a/src/parser/ligodity/AST.ml b/src/parser/ligodity/AST.ml
index 9e24fc74b..4c59ff72d 100644
--- a/src/parser/ligodity/AST.ml
+++ b/src/parser/ligodity/AST.ml
@@ -116,7 +116,7 @@ and declaration =
(* Non-recursive values *)
and let_binding = {
- pattern : pattern;
+ variable : variable;
lhs_type : (colon * type_expr) option;
eq : equal;
let_rhs : expr
@@ -207,7 +207,7 @@ and expr =
| ETuple of (expr, comma) Utils.nsepseq reg
| EPar of expr par reg
| ELetIn of let_in reg
-| EFun of fun_expr
+| EFun of fun_expr reg
| ECond of conditional reg
| ESeq of sequence
@@ -318,33 +318,61 @@ and 'a case_clause = {
rhs : 'a
}
-and let_in = kwd_let * let_binding * kwd_in * expr
+and let_in = {
+ kwd_let : kwd_let;
+ binding : let_in_binding;
+ kwd_in : kwd_in;
+ body : expr
+}
-and fun_expr = (kwd_fun * variable * arrow * expr) reg
+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;
+ arrow : arrow;
+ body : expr
+}
and conditional = {
- kwd_if : kwd_if;
- test : expr;
- kwd_then : kwd_then;
- ifso : expr;
- kwd_else : kwd_else;
- ifnot : expr
+ kwd_if : kwd_if;
+ test : expr;
+ kwd_then : kwd_then;
+ ifso : expr;
+ kwd_else : kwd_else;
+ ifnot : expr
}
(* Projecting regions of the input source code *)
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
Sugar {region; _} | PCons {region; _} -> region
let region_of_pattern = function
PList p -> region_of_list_pattern p
| PTuple {region;_} | PVar {region;_}
-| PUnit {region;_} | PInt {region;_} | PTrue region | PFalse region
+| PUnit {region;_} | PInt {region;_}
+| PTrue region | PFalse region
| PString {region;_} | PWild region
-| PConstr {region; _} | PPar {region;_} | PRecord {region; _}
-| PTyped {region; _} -> region
+| PConstr {region; _} | PPar {region;_}
+| PRecord {region; _} | PTyped {region; _} -> region
let region_of_bool_expr = function
Or {region;_} | And {region;_}
@@ -385,71 +413,6 @@ let region_of_expr = function
| ESeq {region; _} | ERecord {region; _}
| EConstr {region; _} -> region
-(* Rewriting let-expressions and fun-expressions, with some optimisations *)
-
-type sep = Region.t
-
-let ghost_fun, ghost_arrow, ghost_let, ghost_eq, ghost_in =
- let ghost = Region.ghost in ghost, ghost, ghost, ghost, ghost
-
-let norm_fun region kwd_fun pattern eq expr =
- let value =
- match pattern with
- PVar v -> kwd_fun, v, eq, expr
- | _ -> let value = Utils.gen_sym () in
- let fresh = Region.{region=Region.ghost; value} in
- let binding = {pattern; eq;
- lhs_type=None; let_rhs = EVar fresh} in
- let let_in = ghost_let, binding, ghost_in, expr in
- let expr = ELetIn {value=let_in; region=Region.ghost}
- in kwd_fun, fresh, ghost_arrow, expr
- in Region.{region; value}
-
-let norm ?reg (pattern, patterns) sep expr =
- let reg, fun_reg =
- match reg with
- None -> Region.ghost, ghost_fun
- | Some p -> p in
- let apply pattern (sep, expr) =
- ghost_eq, EFun (norm_fun Region.ghost ghost_fun pattern sep expr) in
- let sep, expr = List.fold_right apply patterns (sep, expr)
- in norm_fun reg fun_reg pattern sep expr
-
-(* Unparsing expressions *)
-
-type unparsed = [
- `Fun of (kwd_fun * (pattern Utils.nseq * arrow * expr))
-| `Let of (pattern Utils.nseq * equal * expr)
-| `Idem of expr
-]
-
-(* The function [unparse'] returns a triple [patterns,
- separator_region, expression], and the context (handled by
- [unparse]) decides if [separator_region] is the region of a "="
- sign or "->". *)
-
-let rec unparse' = function
- EFun {value=_,var,arrow,expr; _} ->
- if var.region#is_ghost then
- match expr with
- ELetIn {value = _,{pattern;eq;_},_,expr; _} ->
- if eq#is_ghost then
- let patterns, sep, e = unparse' expr
- in Utils.nseq_cons pattern patterns, sep, e
- else (pattern,[]), eq, expr
- | _ -> assert false
- else if arrow#is_ghost then
- let patterns, sep, e = unparse' expr
- in Utils.nseq_cons (PVar var) patterns, sep, e
- else (PVar var, []), arrow, expr
-| _ -> assert false
-
-let unparse = function
- EFun {value=kwd_fun,_,_,_; _} as e ->
- let binding = unparse' e in
- if kwd_fun#is_ghost then `Let binding else `Fun (kwd_fun, binding)
-| e -> `Idem e
-
(* Printing the tokens with their source locations *)
let print_nsepseq sep print (head,tail) =
@@ -480,16 +443,16 @@ let print_bytes Region.{region; value=lexeme, abstract} =
Printf.printf "%s: Bytes (\"%s\", \"0x%s\")\n"
(region#compact `Byte) lexeme (Hex.to_string abstract)
-let rec print_tokens ?(undo=false) {decl;eof} =
- Utils.nseq_iter (print_statement undo) decl; print_token eof "EOF"
+let rec print_tokens {decl;eof} =
+ Utils.nseq_iter print_statement decl; print_token eof "EOF"
-and print_statement undo = function
+and print_statement = function
Let {value=kwd_let, let_binding; _} ->
print_token kwd_let "let";
- print_let_binding undo let_binding
+ print_let_binding let_binding
| LetEntry {value=kwd_let_entry, let_binding; _} ->
print_token kwd_let_entry "let%entry";
- print_let_binding undo let_binding
+ print_let_binding let_binding
| TypeDecl {value={kwd_type; name; eq; type_expr}; _} ->
print_token kwd_type "type";
print_var name;
@@ -527,9 +490,9 @@ and print_type_par {value={lpar;inside=t;rpar}; _} =
print_type_expr t;
print_token rpar ")"
-and print_projection Region.{value; _} =
- let {struct_name; selector; field_path} = value in
- print_uident struct_name;
+and print_projection node =
+ let {struct_name; selector; field_path} = node in
+ print_var struct_name;
print_token selector ".";
print_nsepseq "." print_selection field_path
@@ -587,28 +550,24 @@ and print_terminator = function
Some semi -> print_token semi ";"
| None -> ()
-and print_let_binding undo {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;
(match lhs_type with
None -> ()
| Some (colon, type_expr) ->
print_token colon ":";
print_type_expr type_expr);
- if undo then
- match unparse let_rhs with
- `Let (patterns, eq, e) ->
- Utils.nseq_iter print_pattern patterns;
- print_token eq "=";
- print_expr undo e
- | `Fun (kwd_fun, (patterns, arrow, e)) ->
- print_token eq "=";
- print_token kwd_fun "fun";
- Utils.nseq_iter print_pattern patterns;
- print_token arrow "->";
- print_expr undo e
- | `Idem _ ->
- print_token eq "="; print_expr undo let_rhs
- else (print_token eq "="; print_expr undo let_rhs)
+ (print_token eq "="; print_expr let_rhs)
and print_pattern = function
PTuple {value=patterns;_} -> print_csv print_pattern patterns
@@ -657,69 +616,62 @@ and print_constr_pattern {value=constr, p_opt; _} =
None -> ()
| Some pattern -> print_pattern pattern
-and print_expr undo = function
- ELetIn {value;_} -> print_let_in undo value
-| ECond cond -> print_conditional undo cond
-| ETuple {value;_} -> print_csv (print_expr undo) value
-| ECase {value;_} -> print_match_expr undo value
-| EFun {value=(kwd_fun,_,_,_) as f; _} as e ->
- if undo then
- let patterns, arrow, expr = unparse' e in
- print_token kwd_fun "fun";
- Utils.nseq_iter print_pattern patterns;
- print_token arrow "->";
- print_expr undo expr
- else print_fun_expr undo f
+and print_expr = function
+ ELetIn {value;_} -> print_let_in value
+| ECond cond -> print_conditional cond
+| ETuple {value;_} -> print_csv print_expr value
+| ECase {value;_} -> print_match_expr value
+| EFun e -> print_fun_expr e
-| EAnnot e -> print_annot_expr undo e
-| ELogic e -> print_logic_expr undo e
-| EArith e -> print_arith_expr undo e
-| EString e -> print_string_expr undo e
+| EAnnot e -> print_annot_expr e
+| ELogic e -> print_logic_expr e
+| EArith e -> print_arith_expr e
+| EString e -> print_string_expr e
| ECall {value=f,l; _} ->
- print_expr undo f; Utils.nseq_iter (print_expr undo) l
+ print_expr f; Utils.nseq_iter print_expr l
| EVar v -> print_var v
-| EProj p -> print_projection p
+| EProj p -> print_projection p.value
| EUnit {value=lpar,rpar; _} ->
print_token lpar "("; print_token rpar ")"
| EBytes b -> print_bytes b
| EPar {value={lpar;inside=e;rpar}; _} ->
- print_token lpar "("; print_expr undo e; print_token rpar ")"
-| EList e -> print_list_expr undo e
-| ESeq seq -> print_sequence undo seq
-| ERecord e -> print_record_expr undo e
+ print_token lpar "("; print_expr e; print_token rpar ")"
+| EList e -> print_list_expr e
+| ESeq seq -> print_sequence seq
+| ERecord e -> print_record_expr e
| EConstr {value=constr,None; _} -> print_uident constr
| EConstr {value=(constr, Some arg); _} ->
- print_uident constr; print_expr undo arg
+ print_uident constr; print_expr arg
-and print_annot_expr undo {value=e,t; _} =
- print_expr undo e;
+and print_annot_expr {value=e,t; _} =
+ print_expr e;
print_token Region.ghost ":";
print_type_expr t
-and print_list_expr undo = function
+and print_list_expr = function
Cons {value={arg1;op;arg2}; _} ->
- print_expr undo arg1;
+ print_expr arg1;
print_token op "::";
- print_expr undo arg2
-| List e -> print_injection (print_expr undo) e
+ print_expr arg2
+| List e -> print_injection print_expr e
(*| Append {value=e1,append,e2; _} ->
- print_expr undo e1;
+ print_expr e1;
print_token append "@";
- print_expr undo e2 *)
+ print_expr e2 *)
-and print_arith_expr undo = function
+and print_arith_expr = function
Add {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "+"; print_expr undo arg2
+ print_expr arg1; print_token op "+"; print_expr arg2
| Sub {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "-"; print_expr undo arg2
+ print_expr arg1; print_token op "-"; print_expr arg2
| Mult {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "*"; print_expr undo arg2
+ print_expr arg1; print_token op "*"; print_expr arg2
| Div {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "/"; print_expr undo arg2
+ print_expr arg1; print_token op "/"; print_expr arg2
| Mod {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "mod"; print_expr undo arg2
-| Neg {value={op;arg}; _} -> print_token op "-"; print_expr undo arg
+ print_expr arg1; print_token op "mod"; print_expr arg2
+| Neg {value={op;arg}; _} -> print_token op "-"; print_expr arg
| Int {region; value=lex,z} ->
print_token region (sprintf "Int %s (%s)" lex (Z.to_string z))
| Mtz {region; value=lex,z} ->
@@ -727,94 +679,96 @@ and print_arith_expr undo = function
| Nat {region; value=lex,z} ->
print_token region (sprintf "Nat %s (%s)" lex (Z.to_string z))
-and print_string_expr undo = function
+and print_string_expr = function
Cat {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "^"; print_expr undo arg2
+ print_expr arg1; print_token op "^"; print_expr arg2
| String s -> print_str s
-and print_logic_expr undo = function
- BoolExpr e -> print_bool_expr undo e
-| CompExpr e -> print_comp_expr undo e
+and print_logic_expr = function
+ BoolExpr e -> print_bool_expr e
+| CompExpr e -> print_comp_expr e
-and print_bool_expr undo = function
+and print_bool_expr = function
Or {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "||"; print_expr undo arg2
+ print_expr arg1; print_token op "||"; print_expr arg2
| And {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "&&"; print_expr undo arg2
-| Not {value={op;arg}; _} -> print_token op "not"; print_expr undo arg
+ print_expr arg1; print_token op "&&"; print_expr arg2
+| Not {value={op;arg}; _} -> print_token op "not"; print_expr arg
| True kwd_true -> print_token kwd_true "true"
| False kwd_false -> print_token kwd_false "false"
-and print_comp_expr undo = function
+and print_comp_expr = function
Lt {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "<"; print_expr undo arg2
+ print_expr arg1; print_token op "<"; print_expr arg2
| Leq {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "<="; print_expr undo arg2
+ print_expr arg1; print_token op "<="; print_expr arg2
| Gt {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op ">"; print_expr undo arg2
+ print_expr arg1; print_token op ">"; print_expr arg2
| Geq {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op ">="; print_expr undo arg2
+ print_expr arg1; print_token op ">="; print_expr arg2
| Neq {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "<>"; print_expr undo arg2
+ print_expr arg1; print_token op "<>"; print_expr arg2
| Equal {value={arg1;op;arg2}; _} ->
- print_expr undo arg1; print_token op "="; print_expr undo arg2
+ print_expr arg1; print_token op "="; print_expr arg2
-and print_record_expr undo e =
- print_injection (print_field_assign undo) e
+and print_record_expr e =
+ print_injection print_field_assign e
-and print_field_assign undo {value; _} =
+and print_field_assign {value; _} =
let {field_name; assignment; field_expr} = value in
print_var field_name;
print_token assignment "=";
- print_expr undo field_expr
+ print_expr field_expr
-and print_sequence undo seq = print_injection (print_expr undo) seq
+and print_sequence seq = print_injection print_expr seq
-and print_match_expr undo expr =
+and print_match_expr expr =
let {kwd_match; expr; opening;
lead_vbar; cases; closing} = expr in
print_token kwd_match "match";
- print_expr undo expr;
+ print_expr expr;
print_opening opening;
print_token_opt lead_vbar "|";
- print_cases undo cases;
+ print_cases cases;
print_closing closing
and print_token_opt = function
None -> fun _ -> ()
| Some region -> print_token region
-and print_cases undo {value; _} =
- print_nsepseq "|" (print_case_clause undo) value
+and print_cases {value; _} =
+ print_nsepseq "|" print_case_clause value
-and print_case_clause undo {value; _} =
+and print_case_clause {value; _} =
let {pattern; arrow; rhs} = value in
print_pattern pattern;
print_token arrow "->";
- print_expr undo rhs
+ print_expr rhs
-and print_let_in undo (kwd_let, let_binding, kwd_in, expr) =
+and print_let_in (bind: let_in) =
+ let {kwd_let; binding; kwd_in; body} = bind in
print_token kwd_let "let";
- print_let_binding undo let_binding;
+ print_let_in_binding binding;
print_token kwd_in "in";
- print_expr undo expr
+ print_expr body
-and print_fun_expr undo (kwd_fun, rvar, arrow, expr) =
+and print_fun_expr {value; _} =
+ let {kwd_fun; param; arrow; body} = value in
print_token kwd_fun "fun";
- print_var rvar;
+ print_var param;
print_token arrow "->";
- print_expr undo expr
+ print_expr body
-and print_conditional undo {value; _} =
+and print_conditional {value; _} =
let open Region in
let {kwd_if; test; kwd_then; ifso; kwd_else; ifnot} = value
in print_token ghost "(";
print_token kwd_if "if";
- print_expr undo test;
+ print_expr test;
print_token kwd_then "then";
- print_expr undo ifso;
+ print_expr ifso;
print_token kwd_else "else";
- print_expr undo ifnot;
+ print_expr ifnot;
print_token ghost ")"
let rec unpar = function
diff --git a/src/parser/ligodity/AST.mli b/src/parser/ligodity/AST.mli
index b2fe8024c..95f5a18c0 100644
--- a/src/parser/ligodity/AST.mli
+++ b/src/parser/ligodity/AST.mli
@@ -118,14 +118,14 @@ and ast = t
and eof = Region.t
and declaration =
- Let of (kwd_let * let_binding) reg (* let p = e *)
-| LetEntry of (kwd_let_entry * let_binding) reg (* let%entry p = e *)
+ Let of (kwd_let * let_binding) reg (* let x = e *)
+| LetEntry of (kwd_let_entry * let_binding) reg (* let%entry x = e *)
| TypeDecl of type_decl reg (* type ... *)
(* Non-recursive values *)
and let_binding = { (* p = e p : t = e *)
- pattern : pattern;
+ variable : variable;
lhs_type : (colon * type_expr) option;
eq : equal;
let_rhs : expr
@@ -216,7 +216,7 @@ and expr =
| ETuple of (expr, comma) Utils.nsepseq reg (* e1, e2, ... *)
| EPar of expr par reg (* (e) *)
| ELetIn of let_in reg (* let p1 = e1 and p2 = e2 and ... in e *)
-| EFun of fun_expr (* fun x -> e *)
+| EFun of fun_expr reg (* fun x -> e *)
| ECond of conditional reg (* if e1 then e2 else e3 *)
| ESeq of sequence (* begin e1; e2; ... ; en end *)
@@ -327,9 +327,26 @@ and 'a case_clause = {
rhs : 'a
}
-and let_in = kwd_let * let_binding * kwd_in * expr
+and let_in = {
+ kwd_let : kwd_let;
+ binding : let_in_binding;
+ kwd_in : kwd_in;
+ body : expr
+}
-and fun_expr = (kwd_fun * variable * arrow * expr) reg
+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;
+ arrow : arrow;
+ body : expr
+}
and conditional = {
kwd_if : kwd_if;
@@ -389,11 +406,11 @@ and conditional = {
keep the region of the original), and the region of the original
"fun" keyword.
*)
-
+(*
type sep = Region.t
val norm : ?reg:(Region.t * kwd_fun) -> pattern Utils.nseq -> sep -> expr -> fun_expr
-
+*)
(* Undoing the above rewritings (for debugging by comparison with the
lexer, and to feed the source-to-source transformations with only
tokens that originated from the original input.
@@ -446,21 +463,6 @@ val norm : ?reg:(Region.t * kwd_fun) -> pattern Utils.nseq -> sep -> expr -> fun
let f l = let n = l in n
*)
-type unparsed = [
- `Fun of (kwd_fun * (pattern Utils.nseq * arrow * expr))
-| `Let of (pattern Utils.nseq * equal * expr)
-| `Idem of expr
-]
-
-val unparse : expr -> unparsed
-
-(* Conversions to type [string] *)
-
-(*
-val to_string : t -> string
-val pattern_to_string : pattern -> string
-*)
-
(* Printing the tokens reconstructed from the AST. This is very useful
for debugging, as the output of [print_token ast] can be textually
compared to that of [Lexer.trace] (see module [LexerMain]). The
@@ -468,14 +470,15 @@ val pattern_to_string : pattern -> string
the AST to be unparsed before printing (those nodes that have been
normalised with function [norm_let] and [norm_fun]). *)
-val print_tokens : ?undo:bool -> ast -> unit
+val print_tokens : (*?undo:bool ->*) ast -> unit
(* Projecting regions from sundry nodes of the AST. See the first
comment at the beginning of this file. *)
-val region_of_pattern : pattern -> Region.t
-val region_of_expr : expr -> Region.t
+val region_of_pattern : pattern -> Region.t
+val region_of_expr : expr -> Region.t
+val region_of_type_expr : type_expr -> Region.t
(* Simplifications *)
@@ -484,3 +487,7 @@ val region_of_expr : expr -> Region.t
contains. *)
val unpar : expr -> expr
+
+(* TODO *)
+
+val print_projection : projection -> unit
diff --git a/src/parser/ligodity/EvalOpt.ml b/src/parser/ligodity/EvalOpt.ml
index 09bf14b48..47731d9c7 100644
--- a/src/parser/ligodity/EvalOpt.ml
+++ b/src/parser/ligodity/EvalOpt.ml
@@ -27,8 +27,7 @@ let help () =
print_endline " (default: .ml)";
print_endline " -e, --eval Interpret .mml or stdin";
print_endline " --raw-edits Do not optimise translation edits";
- print_endline " --verbose= Colon-separated phases: cmdline, lexer,";
- print_endline " parser, unparsing, norm, eval";
+ print_endline " --verbose= Colon-separated phases: cmdline, lexer, parser";
print_endline " --version Short commit hash on stdout";
print_endline " -h, --help This help";
exit 0
diff --git a/src/parser/ligodity/Lexer.mll b/src/parser/ligodity/Lexer.mll
index d3f92a382..85ae4db48 100644
--- a/src/parser/ligodity/Lexer.mll
+++ b/src/parser/ligodity/Lexer.mll
@@ -10,7 +10,6 @@ let sprintf = Printf.sprintf
module Region = Simple_utils.Region
module Pos = Simple_utils.Pos
module SMap = Utils.String.Map
-module SSet = Utils.String.Set
(* Making a natural from its decimal notation (for Tez) *)
@@ -415,7 +414,7 @@ let get_token ?log =
(* TODO: Move out (functor). See LIGO. *)
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
let prerr ~(kind: string) msg =
diff --git a/src/parser/ligodity/Parser.mly b/src/parser/ligodity/Parser.mly
index 052edc526..0bf897599 100644
--- a/src/parser/ligodity/Parser.mly
+++ b/src/parser/ligodity/Parser.mly
@@ -3,6 +3,133 @@
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" *)
+
+let norm_fun_expr patterns expr =
+ let apply pattern expr =
+ match pattern with
+ PVar var ->
+ let fun_expr = {
+ kwd_fun = ghost;
+ param = var;
+ arrow = ghost;
+ body = expr}
+ in EFun (ghost_of fun_expr)
+ | _ -> let fresh = Utils.gen_sym () |> ghost_of in
+ let clause = {pattern; arrow=ghost; rhs=expr} in
+ let clause = ghost_of clause in
+ let cases = ghost_of (clause, []) in
+ let case = {
+ kwd_match = ghost;
+ expr = EVar fresh;
+ opening = With ghost;
+ lead_vbar = None;
+ cases;
+ closing = End ghost} in
+ let case = ECase (ghost_of case) in
+ let fun_expr = {
+ kwd_fun = ghost;
+ param = fresh;
+ arrow = ghost;
+ body = case}
+ in EFun (ghost_of fun_expr)
+ in Utils.nseq_foldr apply patterns expr
+
(* END HEADER *)
%}
@@ -40,15 +167,15 @@ open AST
(* Keywords, symbols, literals and virtual tokens *)
-kwd(X) : oreg(X) { $1 }
-sym(X) : oreg(X) { $1 }
-ident : reg(Ident) { $1 }
-constr : reg(Constr) { $1 }
-string : reg(Str) { $1 }
-eof : oreg(EOF) { $1 }
-vbar : sym(VBAR) { $1 }
-lpar : sym(LPAR) { $1 }
-rpar : sym(RPAR) { $1 }
+kwd(X) : oreg(X) { $1 }
+sym(X) : oreg(X) { $1 }
+ident : reg(Ident) { $1 }
+constr : reg(Constr) { $1 }
+string : reg(Str) { $1 }
+eof : oreg(EOF) { $1 }
+vbar : sym(VBAR) { $1 }
+lpar : sym(LPAR) { $1 }
+rpar : sym(RPAR) { $1 }
lbracket : sym(LBRACKET) { $1 }
rbracket : sym(RBRACKET) { $1 }
lbrace : sym(LBRACE) { $1 }
@@ -127,7 +254,7 @@ sepseq(item,sep):
type_name : ident { $1 }
field_name : ident { $1 }
module_name : constr { $1 }
-struct_name : Ident { $1 }
+struct_name : ident { $1 }
(* Non-empty comma-separated values (at least two values) *)
@@ -146,12 +273,17 @@ list_of(item):
(* Main *)
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:
- reg(kwd(Let) let_binding {$1,$2}) { Let $1 }
-| reg(kwd(LetEntry) let_binding {$1,$2}) { LetEntry $1 }
-| reg(type_decl) { TypeDecl $1 }
+ reg(kwd(LetEntry) entry_binding {$1,$2}) { LetEntry $1, [] }
+| reg(type_decl) { TypeDecl $1, [] }
+| let_declaration { $1 }
(* Type declarations *)
@@ -172,7 +304,7 @@ fun_type:
| reg(arrow_type) { TFun $1 }
arrow_type:
- core_type arrow fun_type { $1,$2,$3 }
+ core_type arrow fun_type { $1,$2,$3 }
core_type:
type_projection {
@@ -182,8 +314,8 @@ core_type:
let arg, constr = $1.value in
let Region.{value=arg_val; _} = arg in
let lpar, rpar = Region.ghost, Region.ghost in
- let arg_val = {lpar; inside=arg_val,[]; rpar} in
- let arg = {arg with value=arg_val} in
+ let value = {lpar; inside=arg_val,[]; rpar} in
+ let arg = {arg with value} in
TApp Region.{$1 with value = constr, arg}
}
| reg(type_tuple type_constr {$1,$2}) {
@@ -191,8 +323,8 @@ core_type:
TApp Region.{$1 with value = constr, arg}
}
| par(cartesian) {
- let Region.{region; value={lpar; inside=prod; rpar}} = $1 in
- TPar Region.{region; value={lpar; inside = TProd prod; rpar}} }
+ let Region.{value={inside=prod; _}; _} = $1 in
+ TPar {$1 with value={$1.value with inside = TProd prod}} }
type_projection:
type_name {
@@ -232,15 +364,46 @@ field_decl:
field_name colon type_expr {
{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:
ident nseq(sub_irrefutable) type_annotation? eq expr {
- let let_rhs = EFun (norm $2 $4 $5) in
- {pattern = PVar $1; lhs_type=$3; eq = Region.ghost; let_rhs}
+ 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
}
| 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:
colon type_expr { $1,$2 }
@@ -255,13 +418,12 @@ sub_irrefutable:
ident { PVar $1 }
| wild { PWild $1 }
| unit { PUnit $1 }
-| par(closed_irrefutable) { PPar $1 }
+| par(closed_irrefutable) { PPar $1 }
closed_irrefutable:
- reg(tuple(sub_irrefutable)) { PTuple $1 }
-| sub_irrefutable { $1 }
-| reg(constr_pattern) { PConstr $1 }
-| reg(typed_pattern) { PTyped $1 }
+ irrefutable { $1 }
+| reg(constr_pattern) { PConstr $1 }
+| reg(typed_pattern) { PTyped $1 }
typed_pattern:
irrefutable colon type_expr { {pattern=$1; colon=$2; type_expr=$3} }
@@ -272,7 +434,7 @@ pattern:
| core_pattern { $1 }
sub_pattern:
- par(tail) { PPar $1 }
+ par(tail) { PPar $1 }
| core_pattern { $1 }
core_pattern:
@@ -283,7 +445,7 @@ core_pattern:
| kwd(True) { PTrue $1 }
| kwd(False) { PFalse $1 }
| string { PString $1 }
-| par(ptuple) { PPar $1 }
+| par(ptuple) { PPar $1 }
| reg(list_of(tail)) { PList (Sugar $1) }
| reg(constr_pattern) { PConstr $1 }
| reg(record_pattern) { PRecord $1 }
@@ -339,11 +501,10 @@ conditional(right_expr):
if_then(right_expr):
kwd(If) expr kwd(Then) right_expr {
- let open Region in
let the_unit = ghost, ghost in
let ifnot = EUnit {region=ghost; value=the_unit} in
{kwd_if=$1; test=$2; kwd_then=$3; ifso=$4;
- kwd_else=Region.ghost; ifnot} }
+ kwd_else=ghost; ifnot} }
if_then_else(right_expr):
kwd(If) expr kwd(Then) closed_if kwd(Else) right_expr {
@@ -369,13 +530,12 @@ match_expr(right_expr):
closing = End Region.ghost}
}
| kwd(MatchNat) expr kwd(With) vbar? reg(cases(right_expr)) {
- let open Region in
let cases = Utils.nsepseq_rev $5.value in
let cast = EVar {region=ghost; value="assert_pos"} in
let cast = ECall {region=ghost; value=cast,($2,[])} in
{kwd_match = $1; expr = cast; opening = With $3;
lead_vbar = $4; cases = {$5 with value=cases};
- closing = End Region.ghost} }
+ closing = End ghost} }
cases(right_expr):
reg(case_clause(right_expr)) { $1, [] }
@@ -386,13 +546,13 @@ case_clause(right_expr):
pattern arrow right_expr { {pattern=$1; arrow=$2; rhs=$3} }
let_expr(right_expr):
- reg(kwd(Let) let_binding kwd(In) right_expr {$1,$2,$3,$4}) {
- ELetIn $1 }
+ 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 let_in = {kwd_let; binding; kwd_in; body}
+ in ELetIn {region; value=let_in} }
fun_expr(right_expr):
- reg(kwd(Fun) nseq(irrefutable) arrow right_expr {$1,$2,$3,$4}) {
- let Region.{region; value = kwd_fun, patterns, arrow, expr} = $1
- in EFun (norm ~reg:(region, kwd_fun) patterns arrow expr) }
+ kwd(Fun) nseq(irrefutable) arrow right_expr { norm_fun_expr $2 $4 }
disj_expr_level:
reg(disj_expr) { ELogic (BoolExpr (Or $1)) }
@@ -531,7 +691,7 @@ module_field:
module_name dot field_name { $1.value ^ "." ^ $3.value }
projection:
- reg(struct_name) dot nsepseq(selection,dot) {
+ struct_name dot nsepseq(selection,dot) {
{struct_name = $1; selector = $2; field_path = $3}
}
| reg(module_name dot field_name {$1,$3})
diff --git a/src/parser/ligodity/ParserMain.ml b/src/parser/ligodity/ParserMain.ml
index cfa5c19d0..5f5481ff6 100644
--- a/src/parser/ligodity/ParserMain.ml
+++ b/src/parser/ligodity/ParserMain.ml
@@ -38,9 +38,8 @@ let tokeniser =
let () =
try
let ast = Parser.program tokeniser buffer in
- if Utils.String.Set.mem "unparsing" options.verbose then
- AST.print_tokens ~undo:true ast
- else () (* AST.print_tokens ast *)
+ if Utils.String.Set.mem "parser" options.verbose
+ then AST.print_tokens ast
with
Lexer.Error diag ->
close_in cin; Lexer.prerr ~kind:"Lexical" diag
diff --git a/src/parser/ligodity/Stubs/Tezos_utils.ml b/src/parser/ligodity/Stubs/Simple_utils.ml
similarity index 100%
rename from src/parser/ligodity/Stubs/Tezos_utils.ml
rename to src/parser/ligodity/Stubs/Simple_utils.ml
diff --git a/src/parser/ligodity/Utils.ml b/src/parser/ligodity/Utils.ml
index 8fd8cc9d2..fd0e7b5a7 100644
--- a/src/parser/ligodity/Utils.ml
+++ b/src/parser/ligodity/Utils.ml
@@ -141,7 +141,7 @@ end
let gen_sym =
let counter = ref 0 in
- fun () -> incr counter; "v" ^ string_of_int !counter
+ fun () -> incr counter; "#" ^ string_of_int !counter
(* General tracing function *)
diff --git a/src/parser/ligodity/Utils.mli b/src/parser/ligodity/Utils.mli
index da758f77b..597f31d89 100644
--- a/src/parser/ligodity/Utils.mli
+++ b/src/parser/ligodity/Utils.mli
@@ -25,73 +25,73 @@ type ('a,'sep) sepseq = ('a,'sep) nsepseq option
(* Consing *)
-val nseq_cons: 'a -> 'a nseq -> 'a nseq
-val nsepseq_cons: 'a -> 'sep -> ('a,'sep) nsepseq -> ('a,'sep) nsepseq
-val sepseq_cons: 'a -> 'sep -> ('a,'sep) sepseq -> ('a,'sep) nsepseq
+val nseq_cons : 'a -> 'a nseq -> 'a nseq
+val nsepseq_cons : 'a -> 'sep -> ('a,'sep) nsepseq -> ('a,'sep) nsepseq
+val sepseq_cons : 'a -> 'sep -> ('a,'sep) sepseq -> ('a,'sep) nsepseq
(* Reversing *)
-val nseq_rev: 'a nseq -> 'a nseq
-val nsepseq_rev: ('a,'sep) nsepseq -> ('a,'sep) nsepseq
-val sepseq_rev: ('a,'sep) sepseq -> ('a,'sep) sepseq
+val nseq_rev : 'a nseq -> 'a nseq
+val nsepseq_rev : ('a,'sep) nsepseq -> ('a,'sep) nsepseq
+val sepseq_rev : ('a,'sep) sepseq -> ('a,'sep) sepseq
(* Rightwards iterators *)
-val nseq_foldl: ('a -> 'b -> 'a) -> 'a -> 'b nseq -> 'a
-val nsepseq_foldl: ('a -> 'b -> 'a) -> 'a -> ('b,'c) nsepseq -> 'a
-val sepseq_foldl: ('a -> 'b -> 'a) -> 'a -> ('b,'c) sepseq -> 'a
+val nseq_foldl : ('a -> 'b -> 'a) -> 'a -> 'b nseq -> 'a
+val nsepseq_foldl : ('a -> 'b -> 'a) -> 'a -> ('b,'c) nsepseq -> 'a
+val sepseq_foldl : ('a -> 'b -> 'a) -> 'a -> ('b,'c) sepseq -> 'a
-val nseq_iter: ('a -> unit) -> 'a nseq -> unit
-val nsepseq_iter: ('a -> unit) -> ('a,'b) nsepseq -> unit
-val sepseq_iter: ('a -> unit) -> ('a,'b) sepseq -> unit
+val nseq_iter : ('a -> unit) -> 'a nseq -> unit
+val nsepseq_iter : ('a -> unit) -> ('a,'b) nsepseq -> unit
+val sepseq_iter : ('a -> unit) -> ('a,'b) sepseq -> unit
(* Leftwards iterators *)
-val nseq_foldr: ('a -> 'b -> 'b) -> 'a nseq -> '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 nseq_foldr : ('a -> 'b -> 'b) -> 'a nseq -> 'b -> 'b
+val nsepseq_foldr : ('a -> 'b -> 'b) -> ('a,'c) nsepseq -> 'b -> 'b
+val sepseq_foldr : ('a -> 'b -> 'b) -> ('a,'c) sepseq -> 'b -> 'b
(* Conversions to lists *)
-val nseq_to_list: 'a nseq -> 'a list
-val nsepseq_to_list: ('a,'b) nsepseq -> 'a list
-val sepseq_to_list: ('a,'b) sepseq -> 'a list
+val nseq_to_list : 'a nseq -> 'a list
+val nsepseq_to_list : ('a,'b) nsepseq -> 'a list
+val sepseq_to_list : ('a,'b) sepseq -> 'a list
(* Effectful symbol generator *)
-val gen_sym: unit -> string
+val gen_sym : unit -> string
(* 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 *)
-val highlight: string -> unit
+val highlight : string -> unit
(* Working with optional values *)
module Option:
sig
- val apply: ('a -> 'b) -> 'a option -> 'b option
- val rev_apply: ('a -> 'a) option -> 'a -> 'a
- val to_string: string option -> string
+ val apply : ('a -> 'b) -> 'a option -> 'b option
+ val rev_apply : ('a -> 'a) option -> 'a -> 'a
+ val to_string : string option -> string
end
(* An extension to the standard module [String] *)
-module String:
+module String :
sig
include module type of String
- module Map: Map.S with type key = t
- module Set: Set.S with type elt = t
+ module Map : Map.S with type key = t
+ module Set : Set.S with type elt = t
end
(* Integer maps *)
-module Int:
+module Int :
sig
type t = int
- module Map: Map.S with type key = t
- module Set: Set.S with type elt = t
+ module Map : Map.S with type key = t
+ module Set : Set.S with type elt = t
end
diff --git a/src/parser/ligodity/Version.ml b/src/parser/ligodity/Version.ml
deleted file mode 100644
index d89964cb1..000000000
--- a/src/parser/ligodity/Version.ml
+++ /dev/null
@@ -1 +0,0 @@
-let version = "UNKNOWN"
diff --git a/src/parser/parser.ml b/src/parser/parser.ml
index b4df5be84..1a259af0f 100644
--- a/src/parser/parser.ml
+++ b/src/parser/parser.ml
@@ -2,7 +2,7 @@ open Trace
module Pascaligo = Parser_pascaligo
module Camligo = Parser_camligo
-(*module Ligodity = Parser_ligodity*)
+module Ligodity = Parser_ligodity
open Parser_pascaligo
module AST_Raw = Parser_pascaligo.AST
diff --git a/src/simplify/dune b/src/simplify/dune
index 5402076af..7035f2eef 100644
--- a/src/simplify/dune
+++ b/src/simplify/dune
@@ -7,7 +7,7 @@
parser
ast_simplified
operators)
- (modules pascaligo camligo simplify)
+ (modules ligodity pascaligo camligo simplify)
(preprocess
(pps
simple-utils.ppx_let_generalized
diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml
index ecd7a55e2..b2e6d1fd5 100644
--- a/src/simplify/ligodity.ml
+++ b/src/simplify/ligodity.ml
@@ -1,8 +1,11 @@
+[@@@warning "-45"]
+
open Trace
open Ast_simplified
module Raw = Parser.Ligodity.AST
module SMap = Map.String
+module Option = Simple_utils.Option
open Combinators
@@ -17,8 +20,8 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value
let type_constants = Operators.Simplify.type_constants
let constants = Operators.Simplify.constants
-let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
- match t with
+let rec simpl_type_expression : Raw.type_expr -> type_expression result =
+ function
| TPar x -> simpl_type_expression x.value.inside
| TAlias v -> (
match List.assoc_opt v.value type_constants with
@@ -82,7 +85,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
ok @@ T_tuple lst
let rec simpl_expression :
- ?te_annot:_ -> Raw.expr -> ae result = fun ?te_annot t ->
+ ?te_annot:type_expression -> Raw.expr -> ae result = fun ?te_annot t ->
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
let simpl_projection = fun (p:Raw.projection) ->
let var =
@@ -100,8 +103,23 @@ let rec simpl_expression :
List.map aux @@ npseq_to_list path in
return @@ E_accessor (var, path')
in
- let open Raw in
+ let mk_let_in binder rhs result =
+ E_let_in {binder; rhs; result} in
+
match t with
+ | Raw.ELetIn e -> (
+ let Raw.{binding; body; _} = e.value in
+ let Raw.{pattern; 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 rhs body)
+ | _ -> let%bind case = simpl_cases [(pattern, body)]
+ in return (E_matching (rhs, case))
+ )
| Raw.EAnnot a -> (
let (expr , type_expr) = a.value in
match te_annot with
@@ -207,7 +225,7 @@ let rec simpl_expression :
@@ npseq_to_list c.value.cases.value in
let%bind cases = simpl_cases lst in
return @@ E_matching (e, cases)
- | _ -> failwith "TOTO"
+ | _ -> failwith "XXX" (* TODO *)
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : annotated_expression result =
let return x = ok @@ make_e_a ?type_annotation:te_annot x in
@@ -330,7 +348,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
let%bind result = simpl_expression return in
let%bind output_type = simpl_type_expression ret_type in
let body = local_declarations @ instructions in
- let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
+ let expression = E_lambda {binder ; input_type = Some input_type;
+ output_type = Some input_type; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name;annotated_expression = {expression;type_annotation}}
)
@@ -369,7 +388,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
let body = tpl_declarations @ local_declarations @ instructions in
let%bind result = simpl_expression return in
- let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
+ let expression = E_lambda {binder ; input_type = Some input_type;
+ output_type = Some output_type; result ; body } in
let type_annotation = Some (T_function (input_type, output_type)) in
ok {name = name.value;annotated_expression = {expression;type_annotation}}
)
@@ -383,9 +403,22 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
let%bind type_expression = simpl_type_expression type_expr in
ok @@ loc x @@ Declaration_type {type_name=name.value;type_expression}
| LetEntry _ -> simple_fail "no entry point yet"
-(* | Let x ->
- let _, binding = x.value in*)
+ | Let x ->
+ let _, binding = x.value in
+ let {pattern; 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
+ match pattern with
+ Raw.PVar v ->
+ let name = v.value in
+ let named_expr = {name; annotated_expression=rhs}
+ in return (Declaration_constant named_expr)
+ | _ -> let%bind case = simpl_cases [(pattern, rhs)]
+ in return (Declaration_constant (E_matching (rhs, case)))
+(*
| ConstDecl x ->
let simpl_const_decl = fun {name;const_type;init} ->
let%bind expression = simpl_expression init in
@@ -400,7 +433,7 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
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_statement : Raw.statement -> instruction result = fun s ->
match s with