Merge branch 'main' into iterscope

spectec/spec/wasm-1.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-2.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config                 hint(show "E")
-relation Step_pure: admininstr* ~> admininstr*  hint(show "E")
-relation Step_read: config ~> admininstr*       hint(show "E")
-relation Steps: config ~>* config               hint(show "E")
+relation Step: config ~> config                 hint(show "E") hint(tabular)
+relation Step_pure: admininstr* ~> admininstr*  hint(show "E") hint(tabular)
+relation Step_read: config ~> admininstr*       hint(show "E") hint(tabular)
+relation Steps: config ~>* config               hint(show "E") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-3.0/2-syntax-aux.watsup

@@ -647,7 +647,7 @@ def $unrolldt(DEF rectype i) = subtype*[i]               -- if $unrollrt(rectype
 
 def $expanddt(deftype) = comptype              -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
-relation Expand: deftype ~~ comptype hint(macro "%expanddt")
+relation Expand: deftype ~~ comptype hint(macro "%expanddt") hint(tabular)
 rule Expand: deftype ~~ comptype               -- if $unrolldt(deftype) = SUB fin typeuse* comptype
 
 

spectec/spec/wasm-3.0/8-reduction.watsup

@@ -2,10 +2,10 @@
 ;; Configurations
 ;;
 
-relation Step: config ~> config       hint(show "E") hint(macro "stepto")
-relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto")
-relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto")
-relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar")
+relation Step: config ~> config       hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_pure: instr* ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Step_read: config ~> instr*  hint(show "E") hint(macro "stepto") hint(tabular)
+relation Steps: config ~>* config     hint(show "E") hint(macro "steptostar") hint(tabular)
 
 rule Step/pure:
   z; instr*  ~>  z; instr'*
@@ -26,7 +26,7 @@ rule Steps/trans:
 
 ;; Expressions
 
-relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar")
+relation Eval_expr: state; expr ~>* state; val*  hint(show "E-expr") hint(macro "steptostar") hint(tabular)
 
 rule Eval_expr:
   z; instr*  ~>*  z'; val*

spectec/spec/wasm-3.0/C-conventions.watsup

@@ -52,7 +52,7 @@ rule NotationTypingInstrScheme/block:
 
 ;; Execution notation
 
-relation NotationReduct: ~> instr*
+relation NotationReduct: ~> instr* hint(tabular)
 
 rule NotationReduct/2:
   ~> (CONST F64 q_1) (CONST F64 q_4) (CONST F64 q_3) $($(BINOP F64 ADD)) $($(BINOP F64 MUL))

spectec/src/al/valid.ml

@@ -63,19 +63,40 @@ let is_trivial_mixop = List.for_all (fun atoms -> List.length atoms = 0)
 let get_deftyps (id: Il.Ast.id) (args: Il.Ast.arg list): deftyp list =
   match Env.find_opt_typ !env id with
   | Some (_, insts) ->
+    let typ_of_arg arg =
+      match (Eval.reduce_arg !env arg).it with
+      | ExpA { it=SubE (_, typ, _); _ } -> typ
+      | ExpA { note; _ } -> note
+      | TypA typ -> typ
+      | a -> failwith ("TODO: " ^ Il.Print.string_of_arg (a $ arg.at))
+    in
+    let get_syntax_arg_name arg = 
+      match arg.it with
+      | Il.Ast.TypA { it=VarT (id, []); _ } -> Some id
+      | _ -> None
+    in
+    let subst_syntax_arg subst arg inst_arg =
+      let name = get_syntax_arg_name inst_arg in
+      if Option.is_some name then
+        let name = Option.get name in
+        Il.Subst.add_typid subst name (typ_of_arg arg)
+      else
+        subst
+    in
+    let subst_inst inst =
+      let InstD (binds, inst_args, deftyp) = inst.it in 
+      let subst = List.fold_left2 subst_syntax_arg Il.Subst.empty args inst_args in
+      let new_args = Il.Subst.subst_args subst inst_args in
+      let new_deftyp = Il.Subst.subst_deftyp subst deftyp in
+      { inst with it = InstD (binds, new_args, new_deftyp) }
+    in
+    let insts = List.map subst_inst insts in
     let get_deftyp inst =
-      let typ_of_arg arg =
-        match (Eval.reduce_arg !env arg).it with
-        | ExpA { it=SubE (_, typ, _); _ } -> typ
-        | ExpA { note; _ } -> note
-        | TypA typ -> typ
-        | a -> failwith ("TODO: " ^ Il.Print.string_of_arg (a $ arg.at))
-      in
-
       let InstD (_, inst_args, deftyp) = inst.it in
-      let args' = List.map typ_of_arg args in
-      let inst_args' = List.map typ_of_arg inst_args in
-      if List.for_all2 (Eval.sub_typ !env) args' inst_args' then
+      let valid_arg arg inst_arg = 
+        Eval.sub_typ !env (typ_of_arg arg) (typ_of_arg inst_arg)
+      in
+      if List.for_all2 valid_arg args inst_args then
         Some deftyp
       else
         None
@@ -254,9 +275,9 @@ let check_struct source typ =
   | VarT (id, args) -> (
     let deftyps = get_deftyps id args in
     if not (List.exists (fun deftyp -> match deftyp.it with StructT _ -> true | _ -> false) deftyps) then
-      error_valid "not a struct" source ""
+      error_valid "not a struct" source (Il.Print.string_of_typ typ)
   )
-  | _ -> error_valid "not a struct" source ""
+  | _ -> error_valid "not a struct" source (Il.Print.string_of_typ typ)
 
 let check_tuple source exprs typ =
   match (ground_typ_of typ).it with
@@ -277,6 +298,40 @@ let check_call source id args result_typ =
       | ExpA expr, ExpP (_, typ') -> check_match source expr.note typ'
       (* Add local variable typ *)
       | TypA typ1, TypP id -> env := Env.bind_var !env id typ1
+      | DefA aid, DefP (_, pparams, ptyp) ->
+        (match Env.find_opt_def !env (aid $ no_region) with
+        | Some (aparams, atyp, _) -> 
+          if not (Eval.sub_typ !env atyp ptyp) then
+            error_valid
+              "argument's return type is not a subtype of parameter's return type"
+              source
+              (Printf.sprintf "  %s !<: %s"
+                (Il.Print.string_of_typ atyp)
+                (Il.Print.string_of_typ ptyp)
+              );
+          List.iter2 (fun aparam pparam ->
+            (* TODO: only supports ExpP for param of arg/param now *)
+            let typ_of_param param =  match param.it with
+            | ExpP (_, typ) -> typ
+            | _ ->
+              error_valid "argument param is not an expression" source
+                (Il.Print.string_of_param aparam);
+            in
+
+            let aptyp = typ_of_param aparam in
+            let pptyp = typ_of_param pparam in
+
+            if not (Eval.sub_typ !env pptyp aptyp) then
+              error_valid
+                "parameter's parameter type is not a subtype of argument's return type"
+                source
+                (Printf.sprintf "  %s !<: %s"
+                  (Il.Print.string_of_typ pptyp)
+                  (Il.Print.string_of_typ aptyp)
+                );
+            ) aparams pparams;
+        | _ -> error_valid "no function definition" source aid
+        );
       | _ ->
         error_valid "argument type mismatch" source
           (Printf.sprintf "  %s =/= %s"
@@ -325,13 +380,15 @@ let check_inv_call source id indices args result_typ =
     | [arg] -> (
       match arg.it with
       | ExpA exp -> exp.note
-      | a -> error_valid (Printf.sprintf "wrong result argument: %s" (Print.string_of_arg (a $ no_region))) source ""
+      | a -> error_valid (Printf.sprintf "wrong result argument")
+        source (Print.string_of_arg (a $ no_region))
     )
     | _ ->
       let arg2typ arg = (
         match arg.it with
         | ExpA exp -> (Il.Ast.VarE ("" $ no_region) $$ no_region % exp.note, exp.note)
-        | a -> error_valid (Printf.sprintf "wrong result argument: %s" (Print.string_of_arg (a $ no_region))) source ""
+        | a -> error_valid (Printf.sprintf "wrong result argument")
+          source (Print.string_of_arg (a $ no_region))
       ) in
       TupT (List.map arg2typ result_args) $ no_region
   in
@@ -537,6 +594,21 @@ let valid_algo (algo: algorithm) =
   |> print_string;
   print_endline ")";
 
+  (* TODO: Use local environment *)
+  (* Store global enviroment *)
+  let global_env = !env in
+
+  (* Add function argument to environment *)
+  (match Env.find_opt_def !env (Al_util.name_of_algo algo $ no_region) with
+  | Some (params, _, _) -> List.iter (fun param ->
+      (match param.it with
+      | DefP (id, params', typ') -> env := Env.bind_def !env id (params', typ', [])
+      | _ -> ()
+      )
+    ) params;
+  | _ -> ()
+  );
+
   init algo;
   let walker =
     { base_unit_walker with
@@ -545,7 +617,10 @@ let valid_algo (algo: algorithm) =
       walk_instr = valid_instr
     }
   in
-  walker.walk_algo walker algo
+  walker.walk_algo walker algo;
+
+  (* Reset global enviroment *)
+  env := global_env
 
 let valid (script: script) =
   List.iter valid_algo script

spectec/src/backend-latex/render.ml

@@ -133,6 +133,7 @@ type env =
     desc_gram : hints ref;
     deco_typ : bool;
     deco_rule : bool;
+    tab_rel : hints ref;
   }
 
 let new_env config =
@@ -155,6 +156,7 @@ let new_env config =
     desc_gram = ref Map.empty;
     deco_typ = false;
     deco_rule = false;
+    tab_rel = ref Map.empty;
   }
 
 let config env : Config.t =
@@ -222,7 +224,8 @@ let env_hintdef env hd =
     env_hints "show" env.show_gram id1 hints
   | RelH (id, hints) ->
     env_hints "macro" env.macro_rel id hints;
-    env_hints "show" env.show_rel id hints
+    env_hints "show" env.show_rel id hints;
+    env_hints "tabular" env.tab_rel id hints
   | VarH (id, hints) ->
     env_hints "macro" env.macro_var id hints;
     env_hints "show" env.show_var id hints
@@ -1402,13 +1405,13 @@ let render_ruledef env d =
   | _ -> failwith "render_ruledef"
 
 
-let render_reddef env d =
+let render_ruledef_tabular env d =
   match d.it with
   | RuleD (id1, id2, e, prems) ->
     let e1, op, e2 =
       match e.it with
       | InfixE (e1, op, e2) -> e1, op, e2
-      | _ -> error e.at "unrecognized format for reduction rule"
+      | _ -> error e.at "unrecognized format for tabular rule, infix operator expected"
     in
     render_rule_deco env "" id1 id2 " \\quad " ^ "& " ^
       render_exp env e1 ^ " &" ^ render_atom env op ^ "& " ^
@@ -1417,7 +1420,7 @@ let render_reddef env d =
         else
           render_conditions env ("\\\\\n  & \\multicolumn{3}{@{}l@{}}{\\qquad " ^
             render_exp env e2 ^ " }") "&&&" prems
-  | _ -> failwith "render_reddef"
+  | _ -> failwith "render_ruledef_tabular"
 
 let render_funcdef env d =
   match d.it with
@@ -1433,20 +1436,6 @@ let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function
   | d::ds -> f d ^ sep ^ render_sep_defs ~sep ~br f ds
 
 
-type rel_sort = TypingRel | ReductionRel
-
-let rec classify_rel e : rel_sort option =
-  match e.it with
-  | InfixE (_, {it = Turnstile; _}, _) -> Some TypingRel
-  | InfixE (_, {it = SqArrow | SqArrowStar | Approx; _}, _) -> Some ReductionRel
-  | InfixE (e1, _, e2) ->
-    (match classify_rel e1 with
-    | None -> classify_rel e2
-    | some -> some
-    )
-  | _ -> None
-
-
 let rec render_defs env = function
   | [] -> ""
   | d::ds' as ds ->
@@ -1470,18 +1459,16 @@ let rec render_defs env = function
     | RelD (_, t, _) ->
       "\\boxed{" ^ render_typ env t ^ "}" ^
       (if ds' = [] then "" else " \\; " ^ render_defs env ds')
-    | RuleD (_, _, e, _) ->
-      (match classify_rel e with
-      | Some TypingRel | None ->
+    | RuleD (id1, _, _, _) ->
+      if Map.mem id1.it !(env.tab_rel) then
+        "\\begin{array}{@{}l@{}r" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
+          render_sep_defs (render_ruledef_tabular env) ds ^
+        "\\end{array}"
+      else
         "\\begin{array}{@{}c@{}}\\displaystyle\n" ^
           render_sep_defs ~sep:"\n\\qquad\n" ~br:"\n\\\\[3ex]\\displaystyle\n"
             (render_ruledef env) ds ^
         "\\end{array}"
-      | Some ReductionRel ->
-        "\\begin{array}{@{}l@{}r" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
-          render_sep_defs (render_reddef env) ds ^
-        "\\end{array}"
-      )
     | DefD _ ->
       "\\begin{array}{@{}l" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
         render_sep_defs (render_funcdef env) ds ^
@@ -1511,13 +1498,13 @@ let rec split_gramdefs gramdefs = function
     | GramD _ -> split_gramdefs (d::gramdefs) ds
     | _ -> List.rev gramdefs, d::ds
 
-let rec split_reddefs id reddefs = function
-  | [] -> List.rev reddefs, []
+let rec split_tabdefs id tabdefs = function
+  | [] -> List.rev tabdefs, []
   | d::ds ->
     match d.it with
     | RuleD (id1, _, _, _) when id1.it = id ->
-      split_reddefs id (d::reddefs) ds
-    | _ -> List.rev reddefs, d::ds
+      split_tabdefs id (d::tabdefs) ds
+    | _ -> List.rev tabdefs, d::ds
 
 let rec split_funcdefs id funcdefs = function
   | [] -> List.rev funcdefs, []
@@ -1541,16 +1528,14 @@ let rec render_script env = function
     | RelD _ ->
       "$" ^ render_def env d ^ "$\n\n" ^
       render_script env ds
-    | RuleD (id1, _, e, _) ->
-      (match classify_rel e with
-      | Some TypingRel | None ->
+    | RuleD (id1, _, _, _) ->
+      if Map.mem id1.it !(env.tab_rel) then
+        let tabdefs, ds' = split_tabdefs id1.it [d] ds in
+        "$$\n" ^ render_defs env tabdefs ^ "\n$$\n\n" ^
+        render_script env ds'
+      else
         "$$\n" ^ render_def env d ^ "\n$$\n\n" ^
         render_script env ds
-      | Some ReductionRel ->
-        let reddefs, ds' = split_reddefs id1.it [d] ds in
-        "$$\n" ^ render_defs env reddefs ^ "\n$$\n\n" ^
-        render_script env ds'
-      )
     | DefD (id, _, _, _) ->
       let funcdefs, ds' = split_funcdefs id.it [d] ds in
       "$$\n" ^ render_defs env funcdefs ^ "\n$$\n\n" ^