motoko-san: monomorphisation

New features:
* monomorphise method calls before translation

New test cases:
* test/viper/polymono.mo

src/mo_types/type.mli

@@ -236,6 +236,8 @@ val glb : typ -> typ -> typ
 
 (* First-order substitution *)
 
+val subst : typ ConEnv.t -> typ -> typ
+
 val close : con list -> typ -> typ
 val close_binds : con list -> bind list -> bind list
 

src/pipeline/pipeline.ml

@@ -509,7 +509,7 @@ let viper_files' parsefn files : viper_result =
   let* () = Typing.check_actors senv progs in
   let prog = CompUnit.combine_progs progs in
   let u = CompUnit.comp_unit_of_prog false prog in
-  let* v = Viper.Trans.unit u in
+  let* v = Viper.Trans.unit (Viper.Prep.prep_unit u) in
   let s = Viper.Pretty.prog_mapped "" v in
   Diag.return s
 

src/viper/README.md

@@ -144,6 +144,7 @@ The implementation of _Motoko-san_ consists of the following source files:
 * `src/viper/syntax.ml` — the Viper AST implementation.
 * `src/viper/pretty.ml` — the Viper pretty printer. Used for serializing Viper AST into text.
 * `src/viper/trans.ml` — the Motoko-to-Viper translation. Implements the logic of _Motoko-san_.
+* `src/viper/prep.ml` —  the Motoko-to-Motoko pass that prepares the unit for translation.
 
 
 Currently supported language features

src/viper/common.ml

@@ -0,0 +1,6 @@
+(* exception for reporting unsupported Motoko syntax *)
+exception Unsupported of Source.region * string
+
+let unsupported at sexp =
+  raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp)))
+

src/viper/prep.ml

@@ -0,0 +1,291 @@
+open Common
+open Source
+open Mo_def.Syntax
+
+module T = Mo_types.Type
+module Cons = Mo_types.Cons
+module Arrange = Mo_def.Arrange
+
+(*
+  Monomorphisation goal. For example, a function call f<Int,Bool>(a,b,c)
+  yields a mono_goal of {id="f", typs=[Int,Bool]}
+*)
+type mono_goal = { mg_id : string; mg_typs : T.typ list; }
+
+let compare_mono_goal (g1 : mono_goal) (g2 : mono_goal) =
+  match String.compare g1.mg_id g2.mg_id with
+  | 0 -> List.compare T.Ord.compare g1.mg_typs g2.mg_typs
+  | ord -> ord
+
+type dec_field_template = { dft_id : string; dft_mk : T.typ list -> dec_field }
+
+let string_of_mono_goal (g : mono_goal) : string =
+  String.concat "$" (g.mg_id :: List.map (fun t ->
+    match T.normalize t with
+    | T.Prim T.Int  -> "Int"
+    | T.Prim T.Nat  -> "Nat"
+    | T.Prim T.Bool -> "Bool"
+    | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)) g.mg_typs)
+
+(*
+  Call monomorphisation function, replacing function calls f<Int,Bool>(a,b,c)
+  with f$Int$Bool(a,b,c) and yielding the corresponding monomorphisation goals.
+*)
+type 'a mono_calls_fn = 'a -> (mono_goal list * 'a)
+
+let rec mono_calls_list (f : 'a mono_calls_fn) : ('a list) mono_calls_fn =
+  function
+    | [] -> ([], [])
+    | (x :: xs) ->
+        let (x_goals, x') = f x in
+        let (xs_goals, xs') = mono_calls_list f xs in
+        (List.append x_goals xs_goals, x' :: xs')
+
+let rec mono_calls_dec_field : dec_field mono_calls_fn =
+  fun df ->
+    let (d_goals, d) = mono_calls_dec df.it.dec in
+    (d_goals, { df with it = { df.it with dec = d }})
+
+and mono_calls_dec : dec mono_calls_fn =
+  function
+    | {it = LetD(p,e,None); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = LetD (p,e',None); at; note})
+    | {it = ExpD(e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = ExpD(e'); at; note})
+    | {it = VarD(x,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = VarD(x,e'); at; note})
+    | d ->
+        (* let _ = print_endline (Wasm.Sexpr.to_string 80 (Arrange.dec d)) in *)
+        ([], d)
+
+and mono_calls_exp : exp mono_calls_fn =
+  function
+    | {it = VarE(x); at; note} -> ([], {it = VarE(x); at; note})
+    | {it = LitE(l); at; note} -> ([], {it = LitE(l); at; note})
+    | {it = FuncE(x,sp,tp,p,t,sugar,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = FuncE(x,sp,tp,p,t,sugar,e'); at; note})
+    | {it = BlockE(ds); at; note} ->
+        let (ds_goals, ds') = mono_calls_list mono_calls_dec ds in
+        (ds_goals, {it = BlockE(ds'); at; note})
+    | {it = AsyncE(s,tb,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = AsyncE(s,tb,e'); at; note})
+    | {it = AnnotE(e,t); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = AnnotE(e',t); at; note})
+    | {it = AssignE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in  (* not sure about the LHS *)
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = AssignE(e1',e2'); at; note} )
+    | {it = ArrayE(mut,es); at; note} ->
+        let (es_goals, es') = mono_calls_list mono_calls_exp es in
+        (es_goals, {it = ArrayE(mut,es'); at; note})
+    | {it = RetE(e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = RetE(e'); at; note})
+    | {it = IfE(e1,e2,e3); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        let (e3_goals, e3') = mono_calls_exp e3 in
+        ( List.concat [e1_goals; e2_goals; e3_goals],
+          {it = IfE(e1',e2',e3'); at; note})
+    | {it = WhileE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = WhileE(e1',e2'); at; note} )
+    | {it = UnE(ot,uo,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = UnE(ot,uo,e'); at; note})
+    | {it = BinE(ot,e1,bo,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = BinE(ot,e1',bo,e2'); at; note} )
+    | {it = RelE(ot,e1,ro,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = RelE(ot,e1',ro,e2'); at; note} )
+    | {it = NotE(e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = NotE(e'); at; note})
+    | {it = AndE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = AndE(e1',e2'); at; note} )
+    | {it = OrE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = OrE(e1',e2'); at; note} )
+    | {it = ImpliesE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = ImpliesE(e1',e2'); at; note} )
+    | {it = TupE(es); at; note} ->
+        let (es_goals, es') = mono_calls_list mono_calls_exp es in
+        (es_goals, {it = TupE(es'); at; note})
+    | {it = AssertE(ak,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = AssertE(ak,e'); at; note})
+    | {it = AwaitE(s,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = AwaitE(s,e'); at; note})
+    | {it = OldE(e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = OldE(e'); at; note})
+    | {it = DotE(e,x); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        (e_goals, {it = DotE(e',x); at; note})
+    | {it = IdxE(e1,e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = IdxE(e1',e2'); at; note} )
+    | {it = CallE({it = VarE v; at = v_at; note = v_note},inst,e); at; note} ->
+        let (e_goals, e') = mono_calls_exp e in
+        let goal = { mg_id = v.it; mg_typs = inst.note } in
+        let call_goals = (if goal.mg_typs == [] then [] else [goal]) in
+        let s = string_of_mono_goal goal in
+        ( List.append call_goals e_goals,
+          {it = CallE({it = VarE (s @@ v_at); at=v_at; note=v_note},
+                      {it = None; at=inst.at; note = []},
+                      e'); at; note} )
+    | {it = CallE(e1,({note=[];_} as inst),e2); at; note} ->
+        let (e1_goals, e1') = mono_calls_exp e1 in
+        let (e2_goals, e2') = mono_calls_exp e2 in
+        ( List.append e1_goals e2_goals,
+          {it = CallE(e1',inst,e2'); at; note} )
+    | e -> unsupported e.at (Arrange.exp e)
+
+module M = Map.Make(String)
+module MonoGoalEnv = Map.Make(struct type t = mono_goal let compare = compare_mono_goal end)
+
+type subst_env = T.typ T.ConEnv.t   (* con -> typ *)
+
+let unwrap_typ_bind_con (tb : typ_bind) : T.con =
+  match tb.note with
+  | None -> unsupported tb.at (Arrange.typ_bind tb)
+  | Some(c) -> c
+
+let init_subst_env (tbs : typ_bind list) (ts : T.typ list) : subst_env =
+  T.ConEnv.from_list2 (List.map unwrap_typ_bind_con tbs) ts
+
+let rec subst_typ env (t : typ) : typ = {t with note = T.subst env t.note}
+and subst_pat env p =
+  { at = p.at;
+    note = T.subst env p.note;
+    it = match p.it with
+      | TupP ps -> TupP (List.map (fun p -> subst_pat env p) ps)
+      | ParP p  -> ParP (subst_pat env p)
+      | AnnotP (p, t) -> AnnotP (subst_pat env p, subst_typ env t)
+      | VarP x -> VarP x
+      | _ -> unsupported p.at (Arrange.pat p) }
+and subst_exp env e =
+  { at = e.at;
+    note = { e.note with note_typ = T.subst env e.note.note_typ };
+    it = match e.it with
+      | VarE(x) -> VarE(x)
+      | LitE(l) -> LitE(l)
+      | UnE(ot,uo,e) -> UnE(ot,uo,subst_exp env e)
+      | BinE(ot,e1,bo,e2) -> BinE(ot,subst_exp env e1,bo,subst_exp env e2)
+      | RelE(ot,e1,ro,e2) -> RelE(ot,subst_exp env e1,ro,subst_exp env e2)
+      | TupE(es) -> TupE(List.map (fun e -> subst_exp env e) es)
+      | DotE(e,x) -> DotE(subst_exp env e,x)
+      | AssignE(e1,e2) -> AssignE(subst_exp env e1, subst_exp env e2)
+      | IdxE(e1,e2) -> IdxE(subst_exp env e1, subst_exp env e2)
+      | WhileE(e1,e2) -> WhileE(subst_exp env e1, subst_exp env e2)
+      | IfE(e1,e2,e3) -> IfE(subst_exp env e1, subst_exp env e2, subst_exp env e3)
+      | BlockE(ds) -> BlockE(List.map (fun d -> subst_dec env d) ds)
+      | RetE(e) -> RetE(subst_exp env e)
+      | CallE(e1,inst,e2) -> CallE(subst_exp env e1, subst_inst env inst, subst_exp env e2)
+      | _ -> unsupported e.at (Arrange.exp e) }
+and subst_dec env d =
+  { at = d.at;
+    note = { d.note with note_typ = T.subst env d.note.note_typ };
+    it = match d.it with
+      | ExpD(e) -> ExpD(subst_exp env e)
+      | LetD(p,e,None) -> LetD(subst_pat env p, subst_exp env e, None)
+      | VarD(x,e) -> VarD(x, subst_exp env e)
+      | _ -> unsupported d.at (Arrange.dec d) }
+and subst_inst env inst =
+  { at = inst.at;
+    note = List.map (fun t -> T.subst env t) inst.note;
+    it = match inst.it with
+      | None -> None
+      | Some (b, ts) ->
+          let ts' = List.map (fun t -> subst_typ env t) ts in
+          Some (b, ts') }
+
+let mk_template_dec_field (df : dec_field) : dec_field_template option =
+  match (df.it.vis.it, df.it.dec.it) with
+    | (Private, LetD({it = VarP(_);at=p_at;note=p_note},
+                     {it = FuncE(x,sp,tp,p,t,sugar,e);
+                      at=fn_at;
+                      note=fn_note},
+                 None)) ->
+      if tp == [] then None else
+      Some({dft_id = x;
+            dft_mk = fun typs ->
+              let env = init_subst_env tp typs in
+              (* let _ = T.ConEnv.iter (fun c t -> print_endline (String.concat " " [Cons.to_string true ":" c; "="; T.string_of_typ t])) env in *)
+              let p' = subst_pat env p in
+              let t' = Option.map (subst_typ env) t in
+              let e' = subst_exp env e in
+              let x' = string_of_mono_goal ({ mg_id = x; mg_typs = typs }) in
+              { df with it = { df.it with dec = { df.it.dec with it =
+                LetD({it = VarP({it=x';at=Source.no_region;note=()});
+                      at=p_at;
+                      note=p_note},
+                     {it = FuncE(x',sp,[],p',t',sugar,e');
+                      at=fn_at;
+                      note=fn_note},
+                  None) } } }
+      })
+    | _ -> None
+
+let mono_partition (dfs : dec_field list) : (dec_field list * dec_field_template M.t) =
+  let (dfs', tmpls) =
+    List.partition_map
+      (fun df ->
+        match mk_template_dec_field df with
+        | None -> Either.Left df
+        | Some(dft) -> Either.Right dft)
+      dfs
+  in
+  let tmpls' = List.fold_left (fun acc tmpl -> M.add tmpl.dft_id tmpl acc) M.empty tmpls in
+  (dfs', tmpls')
+
+let rec mono_iterate (ts : dec_field_template M.t) (dfs : dec_field MonoGoalEnv.t) (goals : mono_goal list) : dec_field MonoGoalEnv.t =
+  match goals with
+  | [] -> dfs
+  | g :: gs ->
+      if MonoGoalEnv.mem g dfs then mono_iterate ts dfs gs else (* skip already instantiated goals *)
+      let df = (M.find g.mg_id ts).dft_mk g.mg_typs in  (* instantiate the goal *)
+      let (gs', df') = mono_calls_dec_field df in       (* collect new goals *)
+      mono_iterate ts (MonoGoalEnv.add g df' dfs) (List.append gs' gs)
+
+let mono_dec_fields (dfs : dec_field list) : dec_field list =
+  let (base_dfs, tmpls) = mono_partition dfs in
+  let (base_goals, base_dfs') = mono_calls_list mono_calls_dec_field base_dfs in
+  let mono_dfs = mono_iterate tmpls MonoGoalEnv.empty base_goals in
+  MonoGoalEnv.fold (fun _ df dfs -> df :: dfs) mono_dfs base_dfs'
+
+let prep_unit (u : comp_unit) : comp_unit =
+  let { imports; body } = u.it in
+  match body.it with
+  | ActorU(id_opt, decs) ->
+    let decs' = mono_dec_fields decs in
+    (* let _ = List.map (fun g -> print_endline (string_of_mono_goal g)) goals in *)
+    let body' = ActorU(id_opt, decs') in
+    (* let _ = List.map (fun d -> print_endline (Wasm.Sexpr.to_string 80 (Arrange.dec_field d))) decs' in *)
+    { u with it = {imports; body = { body with it = body' } } }
+  | _ -> u

src/viper/trans.ml

@@ -1,5 +1,6 @@
 open Source
 
+open Common
 open Syntax
 
 module T = Mo_types.Type
@@ -55,13 +56,6 @@ let rec adjoin ctxt e = function
   | [] -> e
   | f :: fs -> f ctxt (adjoin ctxt e fs)
 
-
-(* exception for reporting unsupported Motoko syntax *)
-exception Unsupported of Source.region * string
-
-let unsupported at sexp =
-  raise (Unsupported (at, (Wasm.Sexpr.to_string 80 sexp)))
-
 type sort = Field | Local | Method
 
 module Env = T.Env

test/viper/ok/polymono.silicon.ok

@@ -0,0 +1,2 @@
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  ([email protected])
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  ([email protected])