Param

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "Ext/libhandler"]
+	path = Ext/libhandler
+	url = https://github.com/koka-lang/libhandler.git

Src/PCompiler/CompilerCore/DefaultTranslationErrorHandler.cs

@@ -53,22 +53,22 @@ public Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplica
                 $"'{duplicate.Name}' duplicates declaration '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
-        public Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
+        public Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing)
         {
             return IssueError(location,
-                $"'{duplicate.Name}' redeclares a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+                $"'{duplicate.Name}' redeclares a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
-        public Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name)
+        public Exception UndeclaredGlobalParam(ParserRuleContext location, string name)
         {
             return IssueError(location,
-                $"'global constant variable {name}' is not undeclared");
+                $"'global param {name}' is not undeclared");
         }
 
-        public Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing)
+        public Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing)
         {
             return IssueError(location,
-                $"try to modify a global constant variable '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
+                $"try to modify a global param '{existing.Name}' at {locationResolver.GetLocation(existing.SourceLocation)}");
         }
 
         public Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount)

Src/PCompiler/CompilerCore/ITranslationErrorHandler.cs

@@ -24,11 +24,11 @@ Exception DuplicateStartState(
 
         Exception DuplicateDeclaration(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
 
-        Exception RedeclareGlobalConstantVariable(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
+        Exception RedeclareGlobalParam(ParserRuleContext location, IPDecl duplicate, IPDecl existing);
 
-        Exception UndeclaredGlobalConstantVariable(ParserRuleContext location, string name);
+        Exception UndeclaredGlobalParam(ParserRuleContext location, string name);
 
-        Exception ModifyGlobalConstantVariable(ParserRuleContext location, IPDecl existing);
+        Exception ModifyGlobalParam(ParserRuleContext location, IPDecl existing);
 
         Exception IncorrectArgumentCount(ParserRuleContext location, int actualCount, int expectedCount);
 

Src/PCompiler/CompilerCore/Parser/PLexer.g4

@@ -59,7 +59,7 @@ THIS      : 'this' ;
 TYPE      : 'type' ;
 VALUES    : 'values' ;
 VAR       : 'var' ;
-CONSTANT       : 'constant' ;
+PARAM       : 'param' ;
 WHILE     : 'while' ;
 WITH      : 'with' ;
 CHOOSE    : 'choose' ;

Src/PCompiler/CompilerCore/Parser/PParser.g4

@@ -60,10 +60,10 @@ topDecl : typeDefDecl
         | namedModuleDecl
         | testDecl
         | implementationDecl
-        | globalValDecl
+        | globalParamDecl
         ;
 
-globalValDecl : CONSTANT idenList COLON type SEMI ;
+globalParamDecl : PARAM idenList COLON type SEMI ;
 
 typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef
             | TYPE name=iden ASSIGN type SEMI # PTypeDef
@@ -255,6 +255,7 @@ param : LPAREN paramBody RPAREN;
 
 testDecl : TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI                  # SafetyTestDecl
          | PARAMTEST globalParam=param testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # ParametricSafetyTestDecl
+         | PARAMTEST globalParam=param ASSUME assumeExpr=expr testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr SEMI # ParametricAssumeSafetyTestDecl
          | TEST testName=iden (LBRACK MAIN ASSIGN mainMachine=iden RBRACK) COLON modExpr REFINES modExpr SEMI  # RefinementTestDecl
          ;
 

Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Function.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
-using System.Linq;
 using Antlr4.Runtime;
 using Plang.Compiler.TypeChecker.AST.Statements;
 
@@ -23,7 +22,6 @@ public class Function : IPDecl, IHasScope
     {
         private readonly HashSet<Function> callees = new HashSet<Function>();
         private readonly HashSet<Function> callers = new HashSet<Function>();
-        private readonly List<Variable> _globalConstantVariables = [];
         private readonly List<Variable> localVariables = new List<Variable>();
         private readonly List<Interface> createsInterfaces = new List<Interface>();
 
@@ -67,24 +65,6 @@ public Function(ParserRuleContext sourceNode) : this("", sourceNode)
 
         public string Name { get; set; }
         public ParserRuleContext SourceLocation { get; }
-
-        public void AddGlobalConstantVariables(ITranslationErrorHandler handler, List<Variable> gvars)
-        {
-            var localNames = localVariables.Select(x => x.Name);
-            // Console.WriteLine("localNames:" + localNames.ToArray());
-            foreach (var g in gvars)
-            {
-                var res = localVariables.Find(x => x.Name == g.Name);
-                if (res == null)
-                {
-                    _globalConstantVariables.Add(g);
-                }
-                else
-                {
-                    throw handler.RedeclareGlobalConstantVariable(res.SourceLocation, res, g);
-                }
-            }
-        }
 
         public void AddLocalVariable(Variable local)
         {

Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/SafetyTest.cs

@@ -1,6 +1,12 @@
 using Antlr4.Runtime;
 using System.Collections.Generic;
 
+public enum TestKind {
+    NormalTest,
+    ParametricTest,
+    AssumeParametricTest,
+}
+
 namespace Plang.Compiler.TypeChecker.AST.Declarations
 {
     public class SafetyTest : IPDecl
@@ -15,6 +21,8 @@ public SafetyTest(ParserRuleContext sourceNode, string testName)
         public IPModuleExpr ModExpr { get; set; }
 
         public IDictionary<string, List<IPExpr>> ParamExpr { get; set; }
+        public IPExpr AssumeExpr { get; set; }
+        public TestKind TestKind { get; set; }
         public string Name { get; }
         public ParserRuleContext SourceLocation { get; }
     }

Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/Variable.cs

@@ -27,6 +27,6 @@ public enum VariableRole
         Param = 1 << 1,
         Field = 1 << 2,
         Temp = 1 << 3,
-        GlobalConstant = 1 << 4
+        GlobalParams = 1 << 4
     }
 }

Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/BoolLiteralExpr.cs

@@ -11,9 +11,19 @@ public BoolLiteralExpr(ParserRuleContext sourceLocation, bool value)
             Value = value;
         }
 
+        public BoolLiteralExpr(bool value)
+        {
+            SourceLocation = ParserRuleContext.EmptyContext;
+            Value = value;
+        }
+
         public bool Value { get; }
 
         public PLanguageType Type { get; } = PrimitiveType.Bool;
         public ParserRuleContext SourceLocation { get; }
+        public override string ToString()
+        {
+            return this.Value.ToString();
+        }
     }
 }

Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/IntLiteralExpr.cs

@@ -11,9 +11,18 @@ public IntLiteralExpr(ParserRuleContext sourceLocation, int value)
             Value = value;
         }
 
+        public IntLiteralExpr(int value)
+        {
+            Value = value;
+        }
+
         public int Value { get; }
 
         public ParserRuleContext SourceLocation { get; }
         public PLanguageType Type { get; } = PrimitiveType.Int;
+        public override string ToString()
+        {
+            return this.Value.ToString();
+        }
     }
 }

Src/PCompiler/CompilerCore/TypeChecker/AST/Expressions/NamedTupleExpr.cs

@@ -14,7 +14,7 @@ public NamedTupleExpr(ParserRuleContext sourceLocation, IReadOnlyList<IPExpr> tu
         }
 
         public IReadOnlyList<IPExpr> TupleFields { get; }
-        
+
         public ParserRuleContext SourceLocation { get; }
 
         public PLanguageType Type { get; }

Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs

@@ -26,14 +26,12 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
 
             // Step 3: Fill function bodies
             var allFunctions = globalScope.GetAllMethods().ToList();
-            // var globalConstantVariables = globalScope.GetVariables();
             foreach (var machineFunction in allFunctions)
             {
                 FunctionBodyVisitor.PopulateMethod(config, machineFunction);
-                // machineFunction.AddGlobalConstantVariables(handler, globalConstantVariables);
                 FunctionValidator.CheckAllPathsReturn(handler, machineFunction);
             }
-           
+
             // Step 2: Validate no static handlers
             foreach (var machine in globalScope.Machines)
             {
@@ -176,7 +174,7 @@ private static Scope BuildGlobalScope(ICompilerConfiguration config, PParser.Pro
             {
                 DeclarationStubVisitor.PopulateStubs(globalScope, programUnit, nodesToDeclarations);
             }
-            
+
             // Step 2: Validate declarations and fill with types
             foreach (var programUnit in programUnits)
             {

Src/PCompiler/CompilerCore/TypeChecker/DeclarationStubVisitor.cs

@@ -30,20 +30,20 @@ public static void PopulateStubs(
             visitor.Visit(context);
         }
 
-        #region GlobalConstantVariables
+        #region GlobalParams
 
-        public override object VisitGlobalValDecl(PParser.GlobalValDeclContext context)
+        public override object VisitGlobalParamDecl(PParser.GlobalParamDeclContext context)
         {
             foreach (var varName in context.idenList()._names)
             {
-                var decl = CurrentScope.Put(varName.GetText(), varName, VariableRole.GlobalConstant);
+                var decl = CurrentScope.Put(varName.GetText(), varName, VariableRole.GlobalParams);
                 nodesToDeclarations.Put(varName, decl);
             }
 
             return null;
         }
 
-        #endregion GlobalConstantVariables 
+        #endregion GlobalParams
 
         #region Events
 
@@ -233,7 +233,7 @@ public override object VisitSafetyTestDecl([NotNull] PParser.SafetyTestDeclConte
             }
             return null;
         }
-        
+
         public override object VisitParametricSafetyTestDecl([NotNull] PParser.ParametricSafetyTestDeclContext context)
         {
             var symbolName = context.testName.GetText();
@@ -243,6 +243,16 @@ public override object VisitParametricSafetyTestDecl([NotNull] PParser.Parametri
             nodesToDeclarations.Put(context, decl);
             return null ;
         }
+
+        public override object VisitParametricAssumeSafetyTestDecl([NotNull] PParser.ParametricAssumeSafetyTestDeclContext context)
+        {
+            var symbolName = context.testName.GetText();
+            var decl = CurrentScope.Put(symbolName, context);
+            if (decl == null) return null;
+            decl.Main = context.mainMachine?.GetText();
+            nodesToDeclarations.Put(context, decl);
+            return null ;
+        }
 
 
         public override object VisitRefinementTestDecl([NotNull] PParser.RefinementTestDeclContext context)

Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs

@@ -16,7 +16,7 @@ public class DeclarationVisitor : PParserBaseVisitor<object>
         private readonly StackProperty<Machine> currentMachine = new StackProperty<Machine>();
         private readonly StackProperty<Scope> currentScope;
         private readonly ParseTreeProperty<IPDecl> nodesToDeclarations;
-        private IDictionary<string, Variable> globalConstantVariables = new Dictionary<string, Variable>();
+        private IDictionary<string, Variable> globalParams = new Dictionary<string, Variable>();
 
         private DeclarationVisitor(
             ITranslationErrorHandler handler,
@@ -26,7 +26,7 @@ private DeclarationVisitor(
             Handler = handler;
             foreach (var variable in topLevelScope.Variables)
             {
-                globalConstantVariables.Add(variable.Name, variable);
+                globalParams.Add(variable.Name, variable);
             }
             currentScope = new StackProperty<Scope>(topLevelScope);
             this.nodesToDeclarations = nodesToDeclarations;
@@ -46,17 +46,17 @@ public static void PopulateDeclarations(
             visitor.Visit(context);
         }
 
-        private void CheckGlobalConstantVariableRedeclare(Variable decl)
+        private void CheckGlobalParamsRedeclare(Variable decl)
         {
-            if (globalConstantVariables.TryGetValue(decl.Name, out var existingDecl))
+            if (globalParams.TryGetValue(decl.Name, out var existingDecl))
             {
-                throw Handler.RedeclareGlobalConstantVariable(decl.SourceLocation, decl, existingDecl); 
+                throw Handler.RedeclareGlobalParam(decl.SourceLocation, decl, existingDecl); 
             }
         }
 
-        #region GlobalConstantVariables 
+        #region GlobalParams
 
-        public override object VisitGlobalValDecl(PParser.GlobalValDeclContext context)
+        public override object VisitGlobalParamDecl(PParser.GlobalParamDeclContext context)
         {
             // COLON type
             var variableType = ResolveType(context.type());
@@ -70,10 +70,10 @@ public override object VisitGlobalValDecl(PParser.GlobalValDeclContext context)
                 currentScope.Value.Update(variable);
             }
             // SEMI
-            return globalConstantVariables;
+            return globalParams;
         } 
 
-        #endregion GlobalConstantVariables 
+        #endregion GlobalParams
 
         #region Events
 
@@ -424,7 +424,7 @@ public override object VisitVarDecl(PParser.VarDeclContext context)
             {
                 var variable = (Variable) nodesToDeclarations.Get(varNameCtxs[i]);
                 // Console.WriteLine("Local Variable:" + variable.Name);
-                CheckGlobalConstantVariableRedeclare(variable);
+                CheckGlobalParamsRedeclare(variable);
                 variable.Type = variableType;
                 variables[i] = variable;
             }

Src/PCompiler/CompilerCore/TypeChecker/ExprVisitor.cs

@@ -22,6 +22,12 @@ public ExprVisitor(Function method, ITranslationErrorHandler handler)
             this.method = method;
             this.handler = handler;
         }
+
+        public ExprVisitor(Scope scope, ITranslationErrorHandler handler)
+        {
+            table = scope;
+            this.handler = handler;
+        }
 
         public override IPExpr VisitPrimitiveExpr(PParser.PrimitiveExprContext context)
         {

Src/PCompiler/CompilerCore/TypeChecker/FunctionBodyVisitor.cs

@@ -54,8 +54,8 @@ public override object VisitFunctionBody(PParser.FunctionBodyContext context)
                 Visit(varDeclContext);
             }
 
-            // Then we validate this scope doesn't redeclare the global constant variables
-            method.Scope.ValidateGlobalConstantVariablesUnique(config.Handler);
+            // Then we validate this scope doesn't redeclare the global params
+            method.Scope.ValidateGlobalParamsUnique(config.Handler);
 
             // Build the statement trees
             var statementVisitor = new StatementVisitor(config, machine, method);