Merge pull request #463 from gfngfn/dev-0-1-0-add-quantifier-to-value…

…-binding

Add the syntax for quantifiers to value bindings

dune-project

@@ -1,6 +1,6 @@
 (lang dune 3.16)
 
-(using menhir 2.1)
+(using menhir 3.0)
 
 (formatting
  (enabled_for dune))

src/dune

@@ -57,8 +57,8 @@
 
 (menhir
  (modules parser dataParser)
- (flags
-  (--table --explain)))
+ (explain true)
+ (flags --table))
 
 (rule
  (targets types.ml)

src/frontend/bytecomp/compiler.ml

@@ -138,7 +138,7 @@ and compile_code_pattern_branch (irpatbr : ir_pattern_branch) : (instruction lis
       IRPatternBranchWhen(irpat, compiled, compiled1)
 
 
-and compile_code_letrec_binding (IRLetRecBinding(var, irpatbr) : ir_letrec_binding) : (instruction list) ir_letrec_binding_scheme =
+and compile_code_let_rec_binding (IRLetRecBinding(var, irpatbr) : ir_let_rec_binding) : (instruction list) ir_let_rec_binding_scheme =
   let comppatbr = compile_code_pattern_branch irpatbr in
   IRLetRecBinding(var, comppatbr)
 
@@ -274,7 +274,7 @@ and compile (ir : ir) (cont : instruction list) =
 
   | IRCodeLetRecIn(irrecbinds, ir2) ->
       let instrs2 = compile ir2 [] in
-      OpCodeLetRec(List.map compile_code_letrec_binding irrecbinds, instrs2) :: cont
+      OpCodeLetRec(List.map compile_code_let_rec_binding irrecbinds, instrs2) :: cont
 
   | IRCodeLetNonRecIn(irpat, ir1, ir2) ->
       let instrs1 = compile ir1 [] in

src/frontend/bytecomp/ir.cppo.ml

@@ -274,7 +274,7 @@ and find_in_environment (env : frame) (evid : EvalVarID.t) : varloc option =
   | None                              -> None
 
 
-and add_letrec_bindings_to_environment (env : frame) (recbinds : letrec_binding list) : (varloc * pattern_branch) list * frame =
+and add_let_rec_bindings_to_environment (env : frame) (recbinds : let_rec_binding list) : (varloc * pattern_branch) list * frame =
   recbinds @|> env @|> map_with_env (fun env recbind ->
     let LetRecBinding(evid, patbr) = recbind in
     let (var, env) = add_to_environment env evid in
@@ -628,7 +628,7 @@ and transform_0 (env : frame) (ast : abstract_tree) : ir * frame =
       end
 
   | LetRecIn(recbinds, ast2) ->
-      let (pairs, env) = add_letrec_bindings_to_environment env recbinds in
+      let (pairs, env) = add_let_rec_bindings_to_environment env recbinds in
       let varir_lst =
         pairs |> List.map (fun pair ->
           let (var, patbr) = pair in

src/frontend/display.ml

@@ -47,7 +47,7 @@ let collect_ids_scheme (fid_ht : unit FreeIDHashTable.t) (frid_ht : LabelSet.t F
           match tv with
           | Updatable({contents = MonoLink(ty)})  -> aux_mono ty
           | Updatable({contents = MonoFree(fid)}) -> aux_free_id fid
-          | MustBeBound(_mbbid)                   -> ()
+          | MustBeBound(mbbid)                    -> aux_bound_id (MustBeBoundID.to_bound_id mbbid)
         end
 
     | DataType(tys, _tyid) ->
@@ -72,9 +72,10 @@ let collect_ids_scheme (fid_ht : unit FreeIDHashTable.t) (frid_ht : LabelSet.t F
     | TypeVariable(ptv) ->
         begin
           match ptv with
-          | PolyFree({contents = MonoLink(ty)})  -> aux_mono ty
-          | PolyFree({contents = MonoFree(fid)}) -> aux_free_id fid
-          | PolyBound(bid)                       -> aux_bound_id bid
+          | PolyFree(Updatable({contents = MonoLink(ty)}))  -> aux_mono ty
+          | PolyFree(Updatable({contents = MonoFree(fid)})) -> aux_free_id fid
+          | PolyFree(MustBeBound(mbbid))                    -> aux_bound_id (MustBeBoundID.to_bound_id mbbid)
+          | PolyBound(bid)                                  -> aux_bound_id bid
         end
 
     | FuncType(poptrow, ptydom, ptycod) ->
@@ -106,7 +107,7 @@ let collect_ids_scheme (fid_ht : unit FreeIDHashTable.t) (frid_ht : LabelSet.t F
     | RowCons(_rlabel, ty, row)                          -> aux_mono ty; aux_mono_row row
     | RowVar(UpdatableRow{contents = MonoRowLink(row)})  -> aux_mono_row row
     | RowVar(UpdatableRow{contents = MonoRowFree(frid)}) -> aux_free_row_id frid
-    | RowVar(MustBeBoundRow(_mbbrid))                    -> ()
+    | RowVar(MustBeBoundRow(mbbrid))                     -> aux_bound_row_id (MustBeBoundRowID.to_bound_id mbbrid)
     | RowEmpty                                           -> ()
 
   and aux_poly_row : poly_row -> unit = function
@@ -395,8 +396,9 @@ and show_mono_row_by_map (dispmap : DisplayMap.t) (row : mono_row) : string opti
 
 let tvf_poly (dispmap : DisplayMap.t) (plev : paren_level) (ptv : poly_type_variable) : string =
   match ptv with
-  | PolyFree(tvuref) -> tvf_mono_updatable dispmap plev !tvuref
-  | PolyBound(bid)   -> dispmap |> DisplayMap.find_bound_id bid
+  | PolyFree(Updatable(tvuref))  -> tvf_mono_updatable dispmap plev !tvuref
+  | PolyFree(MustBeBound(mbbid)) -> dispmap |> DisplayMap.find_bound_id (MustBeBoundID.to_bound_id mbbid)
+  | PolyBound(bid)               -> dispmap |> DisplayMap.find_bound_id bid
 
 
 let rvf_poly (dispmap : DisplayMap.t) (prv : poly_row_variable) : string =

src/frontend/errorReporting.ml

@@ -595,6 +595,13 @@ let make_type_error_message = function
         NormalLine("tests must be stage-1 non-recursive bindings.");
       ]
 
+  | TestMustBeUnitToUnit(rng, pty) ->
+      [
+        NormalLine(Printf.sprintf "at %s:" (Range.to_string rng));
+        NormalLine("tests must be of type unit -> unit, but this one has type");
+        DisplayLine(Display.show_poly_type pty);
+      ]
+
 
 let module_name_chain_to_string (((_, modnm0), modidents) : module_name_chain) =
   let modidents = modidents |> List.map (fun (_, modnm) -> modnm) in

src/frontend/evaluator.cppo.ml

@@ -288,7 +288,7 @@ and interpret_0 (env : environment) (ast : abstract_tree) : syntactic_value =
       end
 
   | LetRecIn(recbinds, ast2) ->
-      let env = add_letrec_bindings_to_environment env recbinds in
+      let env = add_let_rec_bindings_to_environment env recbinds in
       interpret_0 env ast2
 
   | LetNonRecIn(pat, ast1, ast2) ->
@@ -532,7 +532,7 @@ and interpret_1 (env : environment) (ast : abstract_tree) : code_value =
       end
 
   | LetRecIn(recbinds, ast2) ->
-      let (env, cdrecbinds) = interpret_letrec_bindings_1 env recbinds in
+      let (env, cdrecbinds) = interpret_let_rec_bindings_1 env recbinds in
       let code2 = interpret_1 env ast2 in
       CdLetRecIn(cdrecbinds, code2)
 
@@ -1194,7 +1194,7 @@ and check_pattern_matching (env : environment) (pat : pattern_tree) (value_obj :
       None
 
 
-and add_letrec_bindings_to_environment (env : environment) (recbinds : letrec_binding list) : environment =
+and add_let_rec_bindings_to_environment (env : environment) (recbinds : let_rec_binding list) : environment =
   let tris =
     recbinds |> List.map (function LetRecBinding(evid, patbr) ->
       let loc = ref Nil in
@@ -1212,7 +1212,7 @@ and add_letrec_bindings_to_environment (env : environment) (recbinds : letrec_bi
   env
 
 
-and interpret_letrec_bindings_1 (env : environment) (recbinds : letrec_binding list) : environment * code_letrec_binding list =
+and interpret_let_rec_bindings_1 (env : environment) (recbinds : let_rec_binding list) : environment * code_let_rec_binding list =
   (* Generate the symbols for the identifiers and add them to the environment: *)
   let (env, zippedacc) =
     recbinds |> List.fold_left (fun (env, zippedacc) recbind ->
@@ -1245,7 +1245,7 @@ let interpret_bindings_0 ~(run_tests : bool) (env : environment) (binds : bindin
                       add_to_environment env evid (ref value)
 
                   | Rec(recbinds) ->
-                      add_letrec_bindings_to_environment env recbinds
+                      add_let_rec_bindings_to_environment env recbinds
 
                   | Mutable(evid, ast_ini) ->
                       let value_ini = interpret_0 env ast_ini in
@@ -1263,7 +1263,7 @@ let interpret_bindings_0 ~(run_tests : bool) (env : environment) (binds : bindin
                       (env, CdNonRec(symb, code))
 
                   | Rec(recbinds) ->
-                      let (env, cdrecbinds) = interpret_letrec_bindings_1 env recbinds in
+                      let (env, cdrecbinds) = interpret_let_rec_bindings_1 env recbinds in
                       (env, CdRec(cdrecbinds))
 
                   | Mutable(evid, ast) ->

src/frontend/moduleTypechecker.ml

@@ -25,47 +25,6 @@ let abstraction_list (evids : EvalVarID.t list) (ast : abstract_tree) : abstract
   List.fold_right abstraction evids ast
 
 
-let decode_manual_row_base_kind (mnrbkd : manual_row_base_kind) : row_base_kind ok =
-  let open ResultMonad in
-  mnrbkd |> foldM (fun labset (rng, label) ->
-    if labset |> LabelSet.mem label then
-      err (LabelUsedMoreThanOnce(rng, label))
-    else
-      return (labset |> LabelSet.add label)
-  ) LabelSet.empty
-
-
-let add_type_parameters (lev : Level.t) (tyvars : (type_variable_name ranged) list) (typarammap : type_parameter_map) : (type_parameter_map * BoundID.t list) ok =
-  let open ResultMonad in
-  let* (typarammap, bidacc) =
-    tyvars |> foldM (fun (typarammap, bidacc) (rng, tyvarnm) ->
-      if typarammap |> TypeParameterMap.mem tyvarnm then
-        err (TypeParameterBoundMoreThanOnce(rng, tyvarnm))
-      else
-        let mbbid = MustBeBoundID.fresh lev in
-        let bid = MustBeBoundID.to_bound_id mbbid in
-        return (typarammap |> TypeParameterMap.add tyvarnm mbbid, Alist.extend bidacc bid)
-    ) (typarammap, Alist.empty)
-  in
-  return (typarammap, Alist.to_list bidacc)
-
-
-let add_row_parameters (lev : Level.t) (rowvars : (row_variable_name ranged * manual_row_base_kind) list) (rowparammap : row_parameter_map) : (row_parameter_map * BoundRowID.t list) ok =
-  let open ResultMonad in
-  let* (rowparammap, bridacc) =
-    rowvars |> foldM (fun (rowparammap, bridacc) ((rng, rowvarnm), mnbrkd) ->
-      if rowparammap |> RowParameterMap.mem rowvarnm then
-        err (LabelUsedMoreThanOnce(rng, rowvarnm))
-      else
-        decode_manual_row_base_kind mnbrkd >>= fun labset ->
-        let mbbrid = MustBeBoundRowID.fresh lev labset in
-        let brid = MustBeBoundRowID.to_bound_id mbbrid in
-        return (rowparammap |> RowParameterMap.add rowvarnm mbbrid, Alist.extend bridacc brid)
-    ) (rowparammap, Alist.empty)
-  in
-  return (rowparammap, Alist.to_list bridacc)
-
-
 let make_constructor_branch_map (pre : pre) (tyenv : Typeenv.t) (utctorbrs : constructor_branch list) : constructor_branch_map ok =
   let open ResultMonad in
   utctorbrs |> foldM (fun ctormap utctorbr ->
@@ -160,7 +119,8 @@ let add_macro_parameters_to_type_environment (tyenv : Typeenv.t) (pre : pre) (ma
       let (ptybody, beta) =
         let tvid = fresh_free_id pre.quantifiability (Level.succ pre.level) in
         let tvuref = ref (MonoFree(tvid)) in
-        ((rng, TypeVariable(PolyFree(tvuref))), (rng, TypeVariable(Updatable(tvuref))))
+        let tv = Updatable(tvuref) in
+        ((rng, TypeVariable(PolyFree(tv))), (rng, TypeVariable(tv)))
       in
       let (pty, macparamty) =
       match macparam with
@@ -542,7 +502,7 @@ and typecheck_declaration_list (config : typecheck_config) (tyenv : Typeenv.t) (
 and typecheck_declaration (config : typecheck_config) (tyenv : Typeenv.t) (utdecl : untyped_declaration) : (StructSig.t abstracted) ok =
   let open ResultMonad in
   match utdecl with
-  | UTDeclValue(stage, (_, x), (typarams, rowparams), mty) ->
+  | UTDeclValue(stage, (_, x), ManualQuantifier(typarams, rowparams), mty) ->
       let* (typarammap, _) = TypeParameterMap.empty |> add_type_parameters (Level.succ Level.bottom) typarams in
       let* (rowparammap, _) = RowParameterMap.empty |> add_row_parameters (Level.succ Level.bottom) rowparams in
       let pre =
@@ -733,33 +693,9 @@ and typecheck_binding_list (config : typecheck_config) (tyenv : Typeenv.t) (utbi
   return ((quant, ssig), binds)
 
 
-and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (ident : var_name ranged) (utast1 : untyped_abstract_tree) (ty_expected_opt : mono_type option) =
-  let open ResultMonad in
-  let presub = { pre with level = Level.succ pre.level; } in
-  let evid = EvalVarID.fresh ident in
-  let* (e1_raw, ty1) = Typechecker.typecheck presub tyenv utast1 in
-  let e1 = e1_raw in
-  let* () =
-    match ty_expected_opt with
-    | None              -> return ()
-    | Some(ty_expected) -> unify ty1 ty_expected
-  in
-(*
-  let should_be_polymorphic = is_nonexpansive_expression e1 in
-*)
-  let should_be_polymorphic = true in
-    let pty =
-      if should_be_polymorphic then
-        TypeConv.generalize pre.level (TypeConv.erase_range_of_type ty1)
-      else
-        TypeConv.lift_poly (TypeConv.erase_range_of_type ty1)
-    in
-  return (evid, e1, pty)
-
-
 and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind : untyped_binding) : (binding list * StructSig.t abstracted) ok =
   let open ResultMonad in
-  let (_, utbindmain) = utbind in
+  let (rng, utbindmain) = utbind in
   match utbindmain with
   | UTBindValue(attrs, stage, valbind) ->
       let pre =
@@ -778,29 +714,33 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
       in
       if valattr.ValueAttribute.is_test then
         match (stage, valbind) with
-        | (Stage1, UTNonRec(ident, utast1)) ->
-            let (_, test_name) = ident in
-            let ty_expected =
+        | (Stage1, UTNonRec(utletbind)) ->
+            let pty_expected =
               let ty_dom = (Range.dummy "test-dom", BaseType(UnitType)) in
               let ty_cod = (Range.dummy "test-cod", BaseType(UnitType)) in
-              (Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod))
+              Poly(Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod))
             in
-            let* (evid, e1, _pty) = typecheck_nonrec pre tyenv ident utast1 (Some(ty_expected)) in
-            return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty))
+            let* (test_name, pty1, evid, e1) =
+              Typechecker.typecheck_let_nonrec ~always_polymorphic:true pre tyenv utletbind
+            in
+            if TypeConv.poly_type_equal pty_expected pty1 then
+              return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty))
+            else
+              err @@ TestMustBeUnitToUnit(rng, pty1)
 
         | _ ->
-            let rng = Range.dummy "TODO (error): typecheck_binding, test" in
             err @@ TestMustBeStage1NonRec(rng)
       else
         let* (rec_or_nonrecs, ssig) =
           match valbind with
-          | UTNonRec(ident, utast1) ->
-              let* (evid, e1, pty) = typecheck_nonrec pre tyenv ident utast1 None in
+          | UTNonRec(utletbind) ->
+              let* (varnm, pty1, evid, e1) =
+                Typechecker.typecheck_let_nonrec ~always_polymorphic:true pre tyenv utletbind
+              in
               let ssig =
-                let (_, varnm) = ident in
                 let ventry =
                   {
-                    val_type  = pty;
+                    val_type  = pty1;
                     val_name  = Some(evid);
                     val_stage = pre.stage;
                   }
@@ -810,7 +750,7 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
               return ([ NonRec(evid, e1) ], ssig)
 
           | UTRec(utrecbinds) ->
-              let* quints = Typechecker.typecheck_letrec pre tyenv utrecbinds in
+              let* quints = Typechecker.typecheck_let_rec pre tyenv utrecbinds in
               let (recbindacc, ssig) =
                 quints |> List.fold_left (fun (recbindacc, ssig) quint ->
                   let (x, pty, evid, recbind) = quint in
@@ -830,14 +770,12 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
               in
               return ([ Rec(recbindacc |> Alist.to_list) ], ssig)
 
-          | UTMutable((rng, varnm) as var, utastI) ->
-              let* (eI, tyI) = Typechecker.typecheck { pre with quantifiability = Unquantifiable; } tyenv utastI in
-              let evid = EvalVarID.fresh var in
-              let pty = TypeConv.lift_poly (rng, RefType(tyI)) in
+          | UTMutable(ident, utastI) ->
+              let* (varnm, pty_ref, evid, eI) = Typechecker.typecheck_let_mutable pre tyenv ident utastI in
               let ssig =
                 let ventry =
                   {
-                    val_type  = pty;
+                    val_type  = pty_ref;
                     val_name  = Some(evid);
                     val_stage = pre.stage;
                   }