Verified Commit 973d63d7 authored by Julien's avatar Julien
Browse files

[compiler] using __LOC__ in the compiler

parent bec34319
Pipeline #141467468 failed with stage
in 7 minutes and 6 seconds
(* Error Monad *)
Require Import String.
Require Ascii.
Definition linebreak := Eval compute in String.String (Ascii.ascii_of_nat 10) String.EmptyString.
Definition loc := (string*string)%type.
Definition __LOC__ := ("Unknown file","Unknown line")%string.
Definition str_of_loc '(file,line) := ("file "++file++", line "++line)%string.
Inductive exception : Set :=
| Not_found (lab:string)
| Typing (msg:string)
| Overflow
| Should_not_happen
| Should_not_happen (loc:loc)
| Not_yet_implemented (funct:string).
Inductive M (A : Type) : Type :=
......@@ -35,6 +44,10 @@ Proof.
auto.
Qed.
Definition should_not_happen {A} loc := Failed A (Should_not_happen loc).
Open Scope monadic_let_scope.
Fixpoint map {A} {B} (f : A -> M B) (l:list A) : M (list B):=
(fix aux l res :=
......@@ -54,7 +67,9 @@ Definition string_of_exception (e:exception) : string :=
| Not_found lab => "Var '"++lab++"' not found in environment"
| Typing msg => "Typing failure : "++msg
| Overflow => "Integer overflow"
| Should_not_happen => "This exception should never happen, this is a bug"
| Should_not_happen (file,line) =>
"This exception should never happen, this is a bug at file"
++ file ++ " line " ++ line ++". please report."
| Not_yet_implemented funct => "The feature '"++funct++"' has not yet been implemented"
end.
......@@ -54,7 +54,7 @@ Fixpoint michelson_type_of_type (t:ty) : M syntax_type.type :=
| ty_vty (vty_variant lts) =>
(fix michelson_type_of_vty lt :=
match lt with
| nil => Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (_, le)::nil => (michelson_type_of_type le)
| (_, le)::tl => let%err le' := michelson_type_of_type le in
let%err tl' := michelson_type_of_vty tl in
......@@ -82,7 +82,7 @@ Fixpoint michelson_type_of_type (t:ty) : M syntax_type.type :=
| ty_address => Return _ (syntax_type.Comparable_type syntax_type.address)
| ty_contract ty => let%err ty' := michelson_type_of_type ty in
Return _ (syntax_type.contract ty')
| ty_var _ => Failed _ Should_not_happen
| ty_var _ => should_not_happen __LOC__
| ty_key => Return _ syntax_type.key
| ty_signature => Return _ syntax_type.signature
end.
......@@ -122,8 +122,8 @@ Fixpoint michelson_data_of_val_aux (v:value) : M untyped_syntax.concrete_data :=
let 'vty_variant vt := vty in
(fix michelson_data_of_vval lt :=
match lt with
| nil => Failed _ Should_not_happen
| (c', _)::nil => if (eqb_string c c') then (michelson_data_of_val_aux v) else Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (c', _)::nil => if (eqb_string c c') then (michelson_data_of_val_aux v) else should_not_happen __LOC__
| (c', _)::tl => if (eqb_string c c')
then let%err d := michelson_data_of_val_aux v in
Return _ (Left d)
......@@ -167,7 +167,7 @@ Definition michelson_data_of_val (v:value) : M untyped_syntax.concrete_data :=
(* Stack manipulation *)
Fixpoint index_and_remove (x : label) (l : list label) (n : Datatypes.nat) : M (Datatypes.nat * list label) :=
match l with
| nil => Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| hd::tl => if string_dec x hd then Return _ (n, tl)
else let%err (i, tl') := index_and_remove x tl (S n) in
Return _ (i, hd::tl')
......@@ -317,7 +317,7 @@ Definition compile_funct f defs : M (untyped_syntax.instruction) :=
match f with
| fun_var fv => (fix find_fvar (defs: list function) :=
match defs with
| nil => Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (fv', _, ins, _)::tl => if (eqb_string fv fv') then
Return _ ins
else (find_fvar tl)
......@@ -344,8 +344,8 @@ Definition compile_funct f defs : M (untyped_syntax.instruction) :=
let 'vty_variant vt := vty in
(fix compile_variant vt :=
match vt with
| nil => Failed _ Should_not_happen
| (c', t)::nil => if (eqb_string c c') then Return _ NOOP else Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (c', t)::nil => if (eqb_string c c') then Return _ NOOP else should_not_happen __LOC__
| (c', t)::tl => if (eqb_string c c')
then let%err t' :=
michelson_type_of_type (ty_vty (vty_variant tl)) in
......@@ -366,8 +366,8 @@ Definition compile_funct f defs : M (untyped_syntax.instruction) :=
Fixpoint generate_cdrs (l:label) (lt : list (label * ty)) : M untyped_syntax.instruction :=
match lt with
| nil => Failed _ Should_not_happen
| (l', _)::nil => if (eqb_string l l') then Return _ NOOP else Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (l', _)::nil => if (eqb_string l l') then Return _ NOOP else should_not_happen __LOC__
| (l', _)::tl => if (eqb_string l l')
then Return _ CAR
else let%err ins := generate_cdrs l tl in
......@@ -377,12 +377,12 @@ Fixpoint generate_cdrs (l:label) (lt : list (label * ty)) : M untyped_syntax.ins
Fixpoint generate_unpairs (ls : list (label * label)) (ls' : list (label * ty)) (stack : list label) : M (untyped_syntax.instruction * list label) :=
match ls, ls' with
| nil, _ => Return _ (NOOP, stack)
| _, nil => Failed _ Should_not_happen
| _, nil => should_not_happen __LOC__
| (l, x)::nil, (l', _)::nil =>
if (eqb_string l l')
then let%err (dig, stack') := compute_dig x (tln stack 1) in
Return _ (SEQ DROP1 dig, stack')
else Failed _ Should_not_happen
else should_not_happen __LOC__
| (l, x)::tl, (l', _)::tl' =>
if (eqb_string l l')
then let%err (dig, stack') := compute_dig x stack in
......@@ -407,7 +407,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| ty_rty (rty_record lt) =>
let%err ins := generate_cdrs lab lt in
Return _ (SEQ dig ins, tln stack' 1)
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| rhs_update var lx =>
let slx := (LexicoLabSort.sort lx) in
......@@ -417,7 +417,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| ty_rty (rty_record lt) =>
let%err (unpairs, stack'') := generate_unpairs slx lt stack' in
Return _ (SEQ dig unpairs, tln stack'' 1)
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| rhs_add x1 x2 =>
let%err (dig1, stack') := compute_dig x2 stack in
......@@ -475,8 +475,8 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| ty_vty (vty_variant vt) =>
(fix compile_branches vt lbr {struct lbr}:=
match vt, lbr with
| nil, _ => Failed _ Should_not_happen
| _, nil => Failed _ Should_not_happen
| nil, _ => should_not_happen __LOC__
| _, nil => should_not_happen __LOC__
| (_, t)::_ , (pattern_variant c l, rhs)::nil => compile_rhs rhs (l::stack') ((l, t)::stackType') defs
| (_, t)::_ , (pattern_any, rhs)::_ =>
let%err (ins,stack'') := compile_rhs rhs stack' stackType' defs in
......@@ -485,7 +485,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
let%err (insl,_) := (compile_rhs rhs (l::stack') ((l, t)::stackType') defs) in
let%err (insr, stack'') := (compile_branches tl1 tl2) in
Return _ (SEQ dig1 (IF_LEFT insl insr), stack'')
| _, _ => Failed _ Should_not_happen
| _, _ => should_not_happen __LOC__
end) vt lbr
| ty_or ty1 ty2 =>
match lbr with
......@@ -493,7 +493,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
let%err (rhs1', _) := compile_rhs rhs1 (l1::stack') ((l1, ty1)::stackType') defs in
let%err (rhs2', stack'') := compile_rhs rhs2 (l2::stack') ((l2, ty2)::stackType') defs in
Return _ (SEQ dig1 (IF_LEFT rhs1' rhs2'), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_option ty =>
match lbr with
......@@ -501,7 +501,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
let%err (rhs1', _) := compile_rhs rhs1 (l1::stack') ((l1, ty_unit)::stackType') defs in
let%err (rhs2', stack'') := compile_rhs rhs2 (l2::stack') ((l2, ty)::stackType') defs in
Return _ (SEQ dig1 (IF_NONE (SEQ (PUSH syntax_type.unit Unit) rhs1') rhs2'), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_bool =>
match lbr with
......@@ -509,7 +509,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
let%err (rhs1', _) := compile_rhs rhs1 (l1::stack') ((l1, ty_unit)::stackType') defs in
let%err (rhs2', stack'') := compile_rhs rhs2 (l2::stack') ((l2, ty_unit)::stackType') defs in
Return _ (SEQ dig1 (IF_ (SEQ (PUSH syntax_type.unit Unit) rhs1') (SEQ (PUSH syntax_type.unit Unit) rhs2')), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_list ty =>
match lbr with
......@@ -527,9 +527,9 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
let%err (rhs_cons',stack'') :=
compile_rhs rhs_cons (hd::tl::stack') ((hd,ty)::(tl, ty_list ty)::stackType') defs in
Return _ (SEQ dig1 (IF_CONS rhs_cons' (SEQ (DROP 2) rhs_any')),stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| rhs_concat x1 x2 =>
let%err (dig1, stack') := compute_dig x2 stack in
......@@ -576,7 +576,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| rhs_list l =>
let%err (ins, st) := (fix compile_rhs_list l st :=
match l with
| nil => Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| hd::nil => let%err (ty,_) := type_and_remove hd stackType in
let%err mty := michelson_type_of_type ty in
let%err (dig, st') := compute_dig hd (""::st) in
......@@ -597,12 +597,12 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| ty_list ty' => let%err (ins, stack'') :=
compile_rhs r (l2::(tln stack' 1)) ((l2, ty')::stackType) defs in
Return _ (SEQ dig1 (MAP ins), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| rhs_map vars =>
let%err (ins, st') := (fix compile_rhs_list l st :=
match l with
| nil => Failed _ Should_not_happen
| nil => should_not_happen __LOC__
| (l1, l2)::nil =>
let%err (ty1, _) := type_and_remove l1 stackType in
let%err (ty2, _) := type_and_remove l2 stackType in
......@@ -630,7 +630,7 @@ Fixpoint compile_rhs (rhs:rhs) (stack: list label) (stackType : list (label * ty
| ty_map ty1 ty2 => let%err (ins, stack'') :=
compile_rhs r (l1::l2::(tln stack' 1)) ((l1, ty1)::(l2, ty2)::stackType) defs in
Return _ (SEQ dig1 (MAP (SEQ UNPAIR ins)), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| rhs_map_get var l =>
let%err (dig1, stack') := compute_dig var stack in
......@@ -692,9 +692,9 @@ Definition compile_lhs (lhs:lhs) (stack: list label) (t: ty) : M (untyped_syntax
let (n1, stack') := index_and_add x1 stack 1 in
let (n2, stack'') := index_and_add x2 stack' 0 in
Return _ (SEQ UNPAIR (SEQ (DUG n1) (DUG n2)), stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
end.
......@@ -725,8 +725,8 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
| ty_vty (vty_variant vt) =>
(fix compile_branches vt lbr returnStack {struct lbr} :=
match vt, lbr with
| nil, _ => Failed _ Should_not_happen
| _, nil => Failed _ Should_not_happen
| nil, _ => should_not_happen __LOC__
| _, nil => should_not_happen __LOC__
|(_, t)::_,(pattern_variant c l, ins)::nil =>
let (n, stack'') := index_and_add l stack' 0 in
let%err (ins', stack''') := (compile_instr ins stack'' defs) in
......@@ -744,7 +744,7 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
tl1 tl2
(if (List.length returnStack =? 0) then stackl else returnStack) in
Return _ (SEQ dig1 (IF_LEFT (SEQ (DUG n) insl) insr), stackr)
| _::_,_ => Failed _ Should_not_happen
| _::_,_ => should_not_happen __LOC__
end) vt lbr nil
| ty_or _ _ =>
match lbr with
......@@ -755,7 +755,7 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
let%err (ins2', stack2') := compile_instr ins2 stack2 defs in
Return _ (SEQ dig1 (IF_LEFT (SEQ (DUG n1) ins1') (SEQ (DUG n2) ins2')),
if (List.length stack1' =? 0) then stack2' else stack1')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_option _ =>
match lbr with
......@@ -767,7 +767,7 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
Return _ (SEQ dig1 (IF_NONE (SEQ (SEQ (PUSH syntax_type.unit Unit) (DUG n1)) ins1')
(SEQ (DUG n2) ins2')),
if (List.length stack1' =? 0) then stack2' else stack1')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_bool =>
match lbr with
......@@ -779,7 +779,7 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
Return _ (SEQ dig1 (IF_ (SEQ (SEQ (PUSH syntax_type.unit Unit) (DUG n2)) ins2')
(SEQ (SEQ (PUSH syntax_type.unit Unit) (DUG n1)) ins1')),
if (List.length stack1' =? 0) then stack2' else stack1')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_list ty =>
match lbr with
......@@ -799,9 +799,9 @@ Fixpoint compile_instr (ins:typed_instr) (stack : list label) (defs: list functi
let (ntl, stack2) := index_and_add tl stackhd 0 in
let%err (ins_cons',stack'') := compile_instr ins_cons stack2 defs in
Return _ (SEQ dig1 (IF_CONS (SEQ (SEQ (DUG nhd) (DUG ntl)) ins_cons') ins_any'),stack'')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| ty_instr_loop_left _ var var' body _ =>
let%err (dig, stack') := compute_dig var stack in
......
......@@ -471,7 +471,7 @@ Fixpoint remove_tvar_from_val (v:value) (env:g) : M value :=
let%err t' := full_type_from_env (ty_vty vt) env in
match t' with
| ty_vty vt' => Return _ (val_constr c v' vt')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| val_lval (lval_list lv ty) =>
let%err ty' := full_type_from_env ty env in
......@@ -515,7 +515,7 @@ Definition remove_tvar_from_funct (funct:f) (env:g) : M f :=
| fun_constr c vt => let%err t' := full_type_from_env (ty_vty vt) env in
match t' with
| ty_vty vt' => Return _ (fun_constr c vt')
| _ => Failed _ Should_not_happen
| _ => should_not_happen __LOC__
end
| fun_contract ty =>
let%err ty' := full_type_from_env ty env in
......
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