fix reduction bug

Author: Tragicus

apps/cs/src/coq_elpi_cs_hook.mlg

@@ -40,8 +40,16 @@ let elpi_cs_hook program env sigma lhs rhs =
 		 | API.Execute.Success solution ->
 			let gls = Evar.Set.singleton goal_evar in
 			let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
-			let ty_evar, _ = EConstr.destEvar sigma ty in
-			  Some (Evd.remove (Evd.remove sigma ty_evar) goal_evar)
+			if Evd.is_defined sigma goal_evar then
+           let lhs = Reductionops.Stack.zip sigma (EConstr.mkConstU (proji, EConstr.EInstance.empty), Reductionops.Stack.append_app_list (params1 @ [goal]) Reductionops.Stack.empty) in
+           let lhs = Reductionops.whd_const proji env sigma lhs in
+			  let lhs = Reductionops.whd_betaiotazeta env sigma lhs in
+			  let hh, sk1 = EConstr.decompose_app sigma lhs in
+            let () = Feedback.msg_info Pp.(str "aha" ++ Printer.pr_econstr_env env sigma lhs) in
+			  let h2, sk2 = EConstr.decompose_app sigma rhs in
+			  let _, params = EConstr.decompose_app sigma (Retyping.get_type_of env sigma goal) in
+			  Some (sigma, (hh, h2), goal, [], (Array.to_list params, params1), (Array.to_list sk1, Array.to_list sk2), (extra_args1, extra_args2), c1, (None, rhs))
+			else None
 		 | API.Execute.NoMoreSteps
 		 | API.Execute.Failure -> None
     | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None

apps/cs/tests/test_cs.v

@@ -6,16 +6,16 @@ Elpi Override CS All.
 Structure S : Type :=
   { sort :> Type }.
 
-Elpi Accumulate cs.db lp:{{
+Elpi Accumulate canonical_solution lp:{{
 
-cs _ {{ sort lp:Sol }} {{ nat }} :-
-  Sol = {{ Build_S nat }}.
+cs _ {{ sort lp:T }} {{ @id lp:T }} {{ Build_S lp:T (@id lp:T) }}.
 
 }}.
 Elpi Typecheck canonical_solution.
 
 Check 1.
-Check eq_refl _ : (sort _) = nat.
+Check eq_refl _ : (sort nat _) = @id nat.
+Check eq_refl _ : (sort nat _) 1 = @id nat 1.
 Definition nat1 := nat.
 Check 2.
 Check eq_refl _ : (sort _) = nat1.

apps/cs/theories/cs.v

@@ -16,9 +16,9 @@ pred cs i:goal-ctx, o:term, o:term.
 Elpi Tactic canonical_solution.
 Elpi Accumulate lp:{{
 
-solve (goal Ctx _ {{ @eq lp:T lp:Lhs lp:Rhs }} _P []) _ :-
-  cs Ctx Lhs Rhs,
-  % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution".
+solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :-
+  cs Ctx Proj Rhs Sol,
+  % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution".
   true.
 
 }}.