Move towards Expr based interface #84

New Issue

aniva · 2024-06-25T08:13:36-07:00

aniva commented

2024-06-25 08:13:36 -07:00

The sexp interface is good but it requires custom handlers and testing it is cumbersome. We could expose the Lean expr interface to our users directly.

In #83, we have this test

def test_eval (env: Environment): IO LSpec.TestSeq :=
  let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
  runMetaMSeq env do
    let expr ← parseSentence expr
    Meta.forallTelescope expr $ λ _ body => do
      let e ← match Parser.runParserCategory
        (env := ← MonadEnv.getEnv)
        (catName := `term)
        (input := "Or.inl h")
        (fileName := filename) with
        | .ok syn => pure syn
        | .error error => throwError "Failed to parse: {error}"
      let mut tests := LSpec.TestSeq.done
      -- Apply the tactic
      let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
      let target: Expr := mkAnd
        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
      let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target)
      tests := tests ++ test
      let tactic := Tactic.evaluate `h2 e
      let test ← runTermElabMInMeta do
        let newGoals ← runTacticOnMVar tactic goal.mvarId!
        pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target)
      tests := tests ++ test
      return tests

where we test the structure of expressions without using sexp. This should be the new norm.

The `sexp` interface is good but it requires custom handlers and testing it is cumbersome. We could expose the Lean expr interface to our users directly. In https://git.leni.sh/aniva/Pantograph/pulls/83, we have this test ```lean def test_eval (env: Environment): IO LSpec.TestSeq := let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)" runMetaMSeq env do let expr ← parseSentence expr Meta.forallTelescope expr $ λ _ body => do let e ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := "Or.inl h") (fileName := filename) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" let mut tests := LSpec.TestSeq.done -- Apply the tactic let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body let target: Expr := mkAnd (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩)) let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target) tests := tests ++ test let tactic := Tactic.evaluate `h2 e let test ← runTermElabMInMeta do let newGoals ← runTacticOnMVar tactic goal.mvarId! pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target) tests := tests ++ test return tests ``` where we test the structure of expressions without using sexp. This should be the new norm.

aniva added the

part/Serial

category

feature

labels 2024-06-25 08:13:36 -07:00

aniva self-assigned this 2024-06-25 08:13:39 -07:00

aniva commented

2024-08-31 19:50:54 -07:00

Done #85

aniva closed this issue

2024-08-31 19:50:54 -07:00

Sign in to join this conversation.