Support DefA in algorithmic backend

spectec/src/al/al_util.ml

@@ -275,3 +275,4 @@ let handlerT = varT "handler" []
 let stateT = varT "state" []
 let instrT = varT "instr" []
 let admininstrT = varT "admininstr" []
+let funcT = varT "func" []

spectec/src/al/ast.ml

@@ -36,6 +36,7 @@ and value =
   | TupV of value list                 (* tuple of values *)
   | FrameV of value option * value     (* TODO: desugar using CaseV? *)
   | LabelV of value * value            (* TODO: desugar using CaseV? *)
+  | FnameV of id                       (* name of the first order function *)
 
 type extend_dir =                      (* direction of extension *)
   | Front                              (* extend from the front *)
@@ -134,6 +135,7 @@ and arg = arg' phrase
 and arg' =
   | ExpA of expr
   | TypA of typ
+  | DefA of id
 
 (* Instructions *)
 

spectec/src/al/eq.ml

@@ -87,6 +87,7 @@ and eq_arg a1 a2 =
   match a1.it, a2.it with
   | ExpA e1, ExpA e2 -> eq_expr e1 e2
   | TypA typ1, TypA typ2 -> Il.Eq.eq_typ typ1 typ2
+  | DefA id1, DefA id2 -> id1 = id2
   | _ -> false
 
 and eq_args al1 al2 = eq_list eq_arg al1 al2

spectec/src/al/free.ml

@@ -79,7 +79,8 @@ and free_path path =
 and free_arg arg =
   match arg.it with
   | ExpA e -> free_expr e
-  | TypA _ -> IdSet.empty
+  | TypA _
+  | DefA _ -> IdSet.empty
 
 
 (* Instructions *)

spectec/src/al/print.ml

@@ -74,6 +74,7 @@ and string_of_value =
   | StrV r -> string_of_record r
   | OptV (Some e) -> "?(" ^ string_of_value e ^ ")"
   | OptV None -> "?()"
+  | FnameV id -> "$" ^ id
 
 and string_of_values sep = string_of_list string_of_value sep
 
@@ -235,6 +236,7 @@ and string_of_arg arg =
   match arg.it with
   | ExpA e -> string_of_expr e
   | TypA typ -> string_of_typ typ
+  | DefA id -> "$" ^ id
 
 and string_of_args sep = string_of_list string_of_arg sep
 
@@ -400,6 +402,7 @@ let rec structured_string_of_value = function
   | StrV _r -> "StrV (TODO)"
   | OptV None -> "OptV"
   | OptV (Some e) -> "OptV (" ^ structured_string_of_value e ^ ")"
+  | FnameV id -> "FnameV (\"" ^ id ^ "\")"
 
 and structured_string_of_values vl = string_of_list structured_string_of_value ", " vl
 
@@ -561,6 +564,7 @@ and structured_string_of_arg arg =
   match arg.it with
   | ExpA e -> sprintf "ExpA (%s)" (structured_string_of_expr e)
   | TypA typ -> sprintf "TypA (%s)" (string_of_typ typ)
+  | DefA id -> sprintf "DefA (%s)" id
 
 and structured_string_of_args al = string_of_list structured_string_of_arg ", " al
 

spectec/src/al/valid.ml

@@ -45,7 +45,7 @@ module Set = Free.IdSet
 let bound_set: Set.t ref = ref Set.empty
 let add_bound_var id = bound_set := Set.add id !bound_set
 let add_bound_vars expr = bound_set := Set.union (Free.free_expr expr) !bound_set
-let add_bound_param arg = match arg.it with ExpA e -> add_bound_vars e | TypA _ -> ()
+let add_bound_param arg = match arg.it with ExpA e -> add_bound_vars e | TypA _ | DefA _ -> ()
 
 (* Type Env *)
 

spectec/src/al/walk.ml

@@ -18,7 +18,8 @@ type unit_walker = {
 let walk_arg (walker: unit_walker) (arg: arg) : unit =
   match arg.it with
   | ExpA e -> walker.walk_expr walker e
-  | TypA _ -> ()
+  | TypA _
+  | DefA _ -> ()
 
 let walk_iter (walker: unit_walker) (iter: iter) : unit =
   match iter with
@@ -104,7 +105,8 @@ let walk_arg (walker: walker) (arg: arg) : arg =
   let walk_expr = walker.walk_expr walker in
   match arg.it with
   | ExpA e -> { arg with it = ExpA (walk_expr e) }
-  | TypA _ -> arg
+  | TypA _
+  | DefA _ -> arg
 
 let walk_iter (walker: walker) (iter: iter) : iter =
   let walk_expr = walker.walk_expr walker in
@@ -314,7 +316,8 @@ and walk_path f p =
 and walk_arg f a =
   match a.it with
   | ExpA e -> { a with it = ExpA (walk_expr f e) }
-  | TypA _ -> a
+  | TypA _
+  | DefA _ -> a
 
 let rec walk_instr f (instr:instr) : instr list =
   let { pre_instr = pre; post_instr = post; stop_cond_instr = stop_cond; _ } = f in

spectec/src/backend-interpreter/ds.ml

@@ -91,6 +91,7 @@ let lookup_env key env =
     |> freeVar
     |> raise
 
+let lookup_env_opt key env = Env.find_opt key env
 
 (* Info *)
 

spectec/src/backend-interpreter/ds.mli

@@ -8,6 +8,7 @@ val lookup_algo : string -> algorithm
 
 type env = value Env.t
 val lookup_env : string -> env -> value
+val lookup_env_opt : string -> env -> value option
 
 module Store : sig
   val get : unit -> value

spectec/src/backend-interpreter/interpreter.ml

@@ -50,12 +50,16 @@ let transpose matrix =
       new_row :: new_rows in
   transpose' matrix
 
-let extract_exp a =
+let is_not_typarg a =
   match a.it with
-  | ExpA e -> Some e
-  | TypA _ -> None
-let extract_expargs = List.filter_map extract_exp
+  | TypA _ -> false
+  | _ -> true
+let remove_typargs = List.filter is_not_typarg
 
+let dispatch_fname f env =
+  match lookup_env_opt ("$" ^ f) env with
+  | Some (FnameV f') -> f'
+  | _ -> f
 
 let rec create_sub_al_context names iter env =
   let option_name_to_list name = lookup_env name env |> unwrap_optv |> Option.to_list in
@@ -228,17 +232,19 @@ and eval_expr env expr =
     eval_expr env e2 |> unwrap_listv_to_array |> Array.exists ((=) v1) |> boolV
   (* Function Call *)
   | CallE (fname, al) ->
-    let el = extract_expargs al in
-    let args = List.map (eval_expr env) el in
-    (match call_func fname args  with
+    let fname' = dispatch_fname fname env in
+    let el = remove_typargs al in
+    let args = List.map (eval_arg env) el in
+    (match call_func fname' args  with
     | Some v -> v
     | _ -> raise (Exception.MissingReturnValue fname)
     )
   | InvCallE (fname, _, al) ->
-    let el = extract_expargs al in
+    let fname' = dispatch_fname fname env in
+    let el = remove_typargs al in
     (* TODO: refactor numerics function name *)
-    let args = List.map (eval_expr env) el in
-    (match call_func ("inverse_of_"^fname) args  with
+    let args = List.map (eval_arg env) el in
+    (match call_func ("inverse_of_"^fname') args  with
     | Some v -> v
     | _ -> raise (Exception.MissingReturnValue fname)
     )
@@ -423,6 +429,11 @@ and eval_expr env expr =
     boolV (List.length (WasmContext.get_value_stack ()) >= i)
   | _ -> fail_expr expr "cannot evaluate expr"
 
+and eval_arg env a =
+  match a.it with
+  | ExpA e -> eval_expr env e
+  | TypA _ -> assert false
+  | DefA id -> FnameV (dispatch_fname id env)
 
 (* Assignment *)
 
@@ -544,6 +555,11 @@ and assign_split lhs vs env =
     env |> assign ep prefix |> assign es suffix
   )
 
+and assign_param lhs rhs env =
+  match lhs.it with
+  | ExpA e -> assign e rhs env
+  | TypA _ -> assert false
+  | DefA id -> Env.add ("$" ^ id) rhs env
 
 (* Step *)
 
@@ -616,8 +632,8 @@ and step_instr (fname: string) (ctx: AlContext.t) (env: value Env.t) (instr: ins
     let new_env = ctx |> AlContext.get_env |> assign e1 (eval_expr env e2) in
     AlContext.set_env new_env ctx
   | PerformI (f, al) ->
-    let el = extract_expargs al in
-    let args = List.map (eval_expr env) el in
+    let el = remove_typargs al in
+    let args = List.map (eval_arg env) el in
     call_func f args |> ignore;
     ctx
   | TrapI -> raise Exception.Trap
@@ -767,7 +783,7 @@ and create_context (name: string) (args: value list) : AlContext.mode =
   let algo = lookup_algo name in
   let params = params_of_algo algo in
   let body = body_of_algo algo in
-  let params = params |> extract_expargs in
+  let params = params |> remove_typargs in
 
   if List.length args <> List.length params then (
     error
@@ -781,7 +797,7 @@ and create_context (name: string) (args: value list) : AlContext.mode =
 
   let env =
     Env.empty
-    |> List.fold_right2 assign params args
+    |> List.fold_right2 assign_param params args
   in
 
   AlContext.al (name, body, env)

spectec/src/backend-prose/print.ml

@@ -217,6 +217,7 @@ and string_of_arg arg =
   match arg.it with
   | ExpA e -> string_of_expr e
   | TypA typ -> string_of_typ typ
+  | DefA id -> "$" ^ id
 
 and string_of_args sep =
   let string_of_list stringifier sep = function

spectec/src/backend-prose/render.ml

@@ -67,6 +67,7 @@ let a2e a =
   match a.it with
   | Al.Ast.ExpA e -> e
   | Al.Ast.TypA _ -> error a.at "Caannot render inverse function with type argument"
+  | Al.Ast.DefA _ -> error a.at "Caannot render inverse function with def argument"
 
 let al_invcalle_to_al_bine e id nl al =
   let efree = (match e.it with Al.Ast.TupE el -> el | _ -> [ e ]) in
@@ -145,6 +146,8 @@ and al_to_el_arg arg =
   | Al.Ast.TypA _typ ->
     (* TODO: Require Il.Ast.typ to El.Ast.typ translation *)
     Some (El.Ast.(TypA (VarT ("TODO" $ arg.at, []) $ arg.at)))
+  | Al.Ast.DefA id ->
+    Some (El.Ast.DefA (id $ no_region))
 
 and al_to_el_args args =
   List.fold_left

spectec/src/il2al/translate.ml

@@ -60,7 +60,8 @@ let expr2arg e = ExpA e $ e.at
 let arg2expr a =
   match a.it with
   | ExpA e -> e
-  | TypA _ -> error a.at "Argument is not an expression"
+  | TypA _
+  | DefA _ -> error a.at "Argument is not an expression"
 
 (* Utils for IL *)
 let is_case e =
@@ -326,7 +327,7 @@ and translate_args args = List.concat_map ( fun arg ->
   match arg.it with
   | Il.ExpA e -> [ ExpA (translate_exp e) $ arg.at ]
   | Il.TypA typ -> [ TypA typ $ arg.at ]
-  | Il.DefA _ -> [] (* TODO: handle functions *)
+  | Il.DefA id -> [ DefA id.it $ arg.at ]
   | Il.GramA _ -> [] ) args
 
 (* `Il.path` -> `path list` *)
@@ -633,6 +634,7 @@ and call_lhs_to_inverse_call_rhs lhs rhs free_ids =
     match a.it with
     | ExpA e -> contains_ids free_ids e
     | TypA _ -> false
+    | DefA _ -> false
   in
   let rhs2args e =
     (match e.it with

spectec/src/il2al/transpile.ml

@@ -578,13 +578,16 @@ let is_state expr = match expr.note.it with
 
 let is_store_arg arg = match arg.it with
   | ExpA e -> is_store e
-  | TypA _ -> false
+  | TypA _
+  | DefA _ -> false
 let is_frame_arg arg = match arg.it with
   | ExpA e -> is_frame e
-  | TypA _ -> false
+  | TypA _
+  | DefA _ -> false
 let is_state_arg arg = match arg.it with
   | ExpA e -> is_state e
-  | TypA _ -> false
+  | TypA _
+  | DefA _ -> false
 
 let hide_state_args args =
   args
@@ -687,8 +690,8 @@ let remove_state algo =
 let get_state_arg_opt f =
   let arg = ref (TypA (Il.Ast.BoolT $ no_region)) in
   let id = f $ no_region in
-  match Il.Env.find_def !Al.Valid.env id with
-  | (params, _, _) ->
+  match Il.Env.find_opt_def !Al.Valid.env id with
+  | Some (params, _, _) ->
     let param_state = List.find_opt (
       fun param ->
         match param.it with
@@ -699,8 +702,9 @@ let get_state_arg_opt f =
     ) params in
     if Option.is_some param_state then (
       let param_state = Option.get param_state in
-      Option.some {param_state with it = !arg}
-    ) else Option.none
+      Some {param_state with it = !arg}
+    ) else None
+  | None -> None
 
 let recover_state algo =
 
@@ -850,7 +854,7 @@ There are two kinds of auxilirary functions:
 
 (* Case 1 *)
 let handle_framed_algo a instrs =
-  let e_zf = match a.it with | ExpA e -> e | TypA _ -> assert false in
+  let e_zf = match a.it with | ExpA e -> e | TypA _ | DefA _ -> assert false in
   let e_f = match e_zf.it with | TupE [_s; f] -> f | _ -> e_zf in
 
   (* Helpers *)