Merge branch 'duper2' into main

Auto/Embedding/LamBase.lean

@@ -3774,6 +3774,7 @@ def LamWF.bvarApps
   | .nil => wft
   | .cons ty lctx =>
     let lctxr := pushLCtxs (List.reverseAux ex (ty::lctx)) lctx'
+    have lctxr_def : lctxr = pushLCtxs (List.reverseAux ex (ty::lctx)) lctx' := by rfl
     .ofApp _ (LamWF.bvarApps (ex:=ty::ex) wft) (by
       have tyeq : ty = lctxr ex.length := by
         have exlt : List.length ex < List.length (List.reverse (ty :: ex)) := by

Auto/IR/SMT.lean

@@ -330,6 +330,7 @@ inductive Command where
   -- String : Name of datatype
   -- Nat    : Number of parameters of the datatype
   | declDtypes : Array (String × Nat × DatatypeDecl) → Command
+  | echo       : String → Command
   | exit       : Command
 
 def Command.toString : Command → String
@@ -365,6 +366,7 @@ def Command.toString : Command → String
   let sort_decs := String.intercalate " " (infos.data.map (fun (name, args, _) => s!"({SIdent.symb name} {args})"))
   let datatype_decs := String.intercalate " " (infos.data.map (fun (_, _, ddecl) => ddecl.toString))
   s!"(declare-datatypes ({sort_decs}) ({datatype_decs}))"
+| .echo s                              => s!"(echo \"{s}\")"
 | .exit                                => "(exit)"
 
 instance : ToString Command where

Auto/Parser/LexInit.lean

@@ -7,7 +7,22 @@ namespace Auto.Lexer
 -- SMT-LIB2 compilant lexer
 --〈spec_constant〉 ::= 〈numeral〉 | 〈decimal〉 | 〈hexadecimal〉 | 〈binary〉 | 〈string〉
 --〈s_expr 〉 ::= 〈spec_constant〉 | 〈symbol〉 | 〈keyword〉 | ( 〈s_expr〉∗ )
-namespace SMTSexp
+
+-- ⟨index⟩ ::= ⟨numeral⟩ | ⟨symbol⟩
+-- ⟨identifier⟩ ::= ⟨symbol⟩ | (_ ⟨symbol⟩ ⟨index⟩+)
+-- ⟨sort⟩ ::= ⟨identifier⟩ | (⟨identifier⟩ ⟨sort⟩+)
+-- ⟨sorted_var⟩ ::= (⟨symbol⟩ ⟨sort⟩)
+-- ⟨var_binding⟩ ::= (⟨symbol⟩ ⟨term⟩)
+-- ⟨term⟩ ::= ⟨spec_constant⟩ | (forall (⟨sorted_var⟩+) ⟨term⟩) | (exists (⟨sorted_var⟩+) ⟨term⟩) | (let (⟨var_binding⟩+) ⟨term⟩)
+
+/- Ignored for now:
+    - Attributes
+    - Qual_identifiers
+    - Patterns
+    - Match_cases
+    - Some of the Term forms that require any of the above -/
+
+namespace SMT
 
 open Regex
 
@@ -62,6 +77,12 @@ def lparen : ERE := .inStr "("
 
 def rparen : ERE := .inStr ")"
 
+def underscore : ERE := .ofStr "_"
+
+def SMTforall : ERE := .ofStr "forall"
+def SMTexists : ERE := .ofStr "exists"
+def SMTlet : ERE := .ofStr "let"
+
 /-- Special constants -/
 def specConst : ERE := .plus #[
   .attr numeral "numeral",
@@ -71,7 +92,7 @@ def specConst : ERE := .plus #[
   .attr string "string"
 ]
 
-def lexicons : ERE := .plus #[
+def sexpr : ERE := .plus #[
   specConst,
   -- For lexical analysis, do not distinguish between keyword and symbol
   symbol,
@@ -81,22 +102,63 @@ def lexicons : ERE := .plus #[
   .attr comment "comment"
 ]
 
-/-
+-- ⟨index⟩ ::= ⟨numeral⟩ | ⟨symbol⟩
+def index : ERE := .plus #[
+  .attr numeral "numeral",
+  symbol
+]
 
-#eval string.toADFA
+-- ⟨identifier⟩ ::= ⟨symbol⟩ | (_ ⟨symbol⟩ ⟨index⟩+)
+def identifier : ERE := .plus #[
+  symbol,
+  .attr lparen "(",
+  .attr underscore "_",
+  .attr rparen ")",
+  index
+]
 
-#eval specConst.toADFA
+-- ⟨sort⟩ ::= ⟨identifier⟩ | (⟨identifier⟩ ⟨sort⟩+)
+def sort : ERE := .plus #[
+  identifier,
+  .attr lparen "(",
+  .attr rparen ")"
+]
 
--- Good property: Each state have at most one attribute!
-#eval lexicons.toADFA
+-- ⟨sorted_var⟩ ::= (⟨symbol⟩ ⟨sort⟩)
+def sorted_var : ERE := .plus #[
+  symbol,
+  .attr lparen "(",
+  .attr rparen ")",
+  sort
+]
 
+-- ⟨term⟩ ::= ⟨spec_constant⟩ | ⟨forall (⟨sorted_var⟩+) ⟨term⟩ | ⟨exists (⟨sorted_var⟩+) ⟨term⟩
+def term : ERE := .plus #[
+  specConst,
+  .attr SMTforall "forall",
+  .attr SMTexists "exists",
+  .attr SMTlet "let",
+  .attr lparen "(",
+  .attr rparen ")",
+  sorted_var
+]
+
+-- Good property: Each state have at most one attribute!
+/-
+#eval string.toADFA
+#eval specConst.toADFA
+#eval sexpr.toADFA
+#eval identifier.toADFA -- State 6 has two attributes, not sure if that's a problem
+#eval sort.toADFA -- State 6 has two attributes, not sure if that's a problem
+#eval sorted_var.toADFA -- State 6 has two attributes, not sure if that's a problem
+#eval term.toADFA -- States 9, 36, and 37 have multiple attributes, not sure if that's a problem
 -/
 
 local instance : Hashable Char where
   hash c := hash c.val
 
-initialize lexiconADFA : ADFA Char ← pure lexicons.toADFA
+initialize lexiconADFA : ADFA Char ← pure term.toADFA
 
-end SMTSexp
+end SMT
 
 end Auto.Lexer