Refactor all tactics using new proof engine.

 + disconnect type classes
 + reconnect legacy ring

.gitignore

@@ -11,6 +11,7 @@ _build
 setup.data
 setup.log
 /attic
+/theories/attic
 
 /system/*.o
 /system/callprover
@@ -31,6 +32,7 @@ setup.log
 
 /doc/easycrypt.pdf
 
+/webui/workspace/
 /webui/webui-env/
 /webui/econline.egg-info/
 /webui/build/

_tags

@@ -7,7 +7,6 @@ true : bin_annot
 
 # --------------------------------------------------------------------
 <src>            : include
-<src/newengine>  : include
 <src/phl>        : include
 <src/extraction> : include
 

src/ecAlgTactic.ml

@@ -3,6 +3,7 @@ open EcUtils
 open EcTypes
 open EcFol
 open EcDecl
+open EcCoreGoal
 open EcAlgebra
 
 (* -------------------------------------------------------------------- *)
@@ -147,85 +148,47 @@ let ring_axioms  = Axioms.ring_axioms
 let field_axioms = Axioms.field_axioms
 
 (* -------------------------------------------------------------------- *)
-open EcBaseLogic
-open EcLogic
-open EcReduction
-
-class rn_ring_congr = object inherit xrule "ring_congr"  end
-class rn_ring_norm  = object inherit xrule "ring_norm"  end
-class rn_ring       = object inherit xrule "ring"  end
-class rn_field      = object inherit xrule "field" end
-
-let rn_ring_congr = RN_xtd (new rn_ring_congr)
-let rn_ring_norm  = RN_xtd (new rn_ring_norm) 
-let rn_ring       = RN_xtd (new rn_ring)
-let rn_field      = RN_xtd (new rn_field)
-
-let n_ring_congr juc hyps (cr:cring) (rm:RState.rstate) f li lv =
-  let pe,rm = toring hyps cr rm f in
-  let rm' = RState.update rm li lv in
-  let env = EcEnv.LDecl.toenv hyps in
-  let mk_goal i =
-    let r1 = oget (RState.get i rm) in
-    let r2 = oget (RState.get i rm') in
-    EqTest.for_type_exn env r1.f_ty r2.f_ty;
-    f_eq r1 r2 in 
-  let f' = ofring (ring_of_cring cr) rm' pe in
-  let g = new_goal juc (hyps, f_eq f f') in
-  let sg = List.map mk_goal li in
-  let gs = prove_goal_by sg rn_ring_congr g in
-  f', snd g, gs
-
-let n_ring_norm juc hyps (cr:cring) (rm:RState.rstate) f =
-  let pe, rm = toring hyps cr rm f in
-  let ofring = ofring (ring_of_cring cr) rm in
-  let npe    = ring_simplify_pe cr [] pe in
-  let f'     = ofring npe in
-  let g      = new_goal juc (hyps, f_eq f f') in
-  let gs     = prove_goal_by [] rn_ring_norm g in
-  rm, f', snd g, gs
-
-let t_ring_simplify cr eqs (f1, f2) g =
-  let hyps = get_hyps g in
+let is_module_loaded env =
+  List.for_all
+    (fun x -> EcEnv.Theory.by_path_opt x env <> None)
+    Axioms.tmod_and_deps
+
+(* -------------------------------------------------------------------- *)
+let t_ring_simplify cr eqs (f1, f2) tc =
+  let hyps = FApi.tc1_hyps tc in
   let cr = cring_of_ring cr in
   let f1 = ring_simplify hyps cr eqs f1 in
   let f2 = ring_simplify hyps cr eqs f2 in
-	prove_goal_by [f_eq f1 f2] rn_ring g
+  FApi.xmutate1 tc `Ring [f_eq f1 f2]
 
-let t_ring r eqs (f1, f2) g =
-  let hyps = get_hyps g in
+let t_ring r eqs (f1, f2) tc =
+  let hyps = FApi.tc1_hyps tc in
   let cr = cring_of_ring r in
   let f  = ring_eq hyps cr eqs f1 f2 in
-  if   EcReduction.is_conv (get_hyps g) f (emb_rzero r)
-  then prove_goal_by [] rn_ring g
-  else prove_goal_by [f_eq f (emb_rzero r)] rn_ring g
+  if   EcReduction.is_conv hyps f (emb_rzero r)
+  then FApi.xmutate1 tc `Ring []
+  else FApi.xmutate1 tc `Ring [f_eq f (emb_rzero r)]
 
-let t_field_simplify r eqs (f1, f2) g =
-  let hyps = get_hyps g in
+let t_field_simplify r eqs (f1, f2) tc =
+  let hyps = FApi.tc1_hyps tc in
   let cr = cfield_of_field r in
   let (c1, n1, d1) = field_simplify hyps cr eqs f1 in
   let (c2, n2, d2) = field_simplify hyps cr eqs f2 in
 
   let c = List.map (fun f -> f_not (f_eq f (emb_fzero r))) (c1 @ c2) in
   let f = f_eq (fdiv r n1 d1) (fdiv r n2 d2) in
 
-    prove_goal_by (c @ [f]) rn_field g
+  FApi.xmutate1 tc `Field (c @ [f])
 
-let t_field r eqs (f1, f2) g =
-  let hyps = get_hyps g in
+let t_field r eqs (f1, f2) tc =
+  let hyps = FApi.tc1_hyps tc in
   let cr = cfield_of_field r in
   let (c, (n1, n2), (d1, d2)) = field_eq hyps cr eqs f1 f2 in
   let c  = List.map (fun f -> f_not (f_eq f (emb_fzero r))) c in
   let r1 = fmul r n1 d2
   and r2 = fmul r n2 d1 in
   let f  = ring_eq hyps (cring_of_ring r.f_ring) eqs r1 r2 in
 
-    if   EcReduction.is_conv (get_hyps g) f (emb_fzero r)
-    then prove_goal_by c rn_field g
-    else prove_goal_by (c @ [f_eq f (emb_fzero r)]) rn_field g
-
-(* -------------------------------------------------------------------- *)
-let is_module_loaded env =
-  List.for_all
-    (fun x -> EcEnv.Theory.by_path_opt x env <> None)
-    Axioms.tmod_and_deps
+  if   EcReduction.is_conv hyps f (emb_fzero r)
+  then FApi.xmutate1 tc `Field []
+  else FApi.xmutate1 tc `Field (c @ [f_eq f (emb_fzero r)])

src/ecAlgTactic.mli

@@ -3,8 +3,8 @@ open EcSymbols
 open EcTypes
 open EcDecl
 open EcFol
-open EcLogic
 open EcAlgebra
+open EcCoreGoal
 
 (* -------------------------------------------------------------------- *)
 val is_module_loaded : EcEnv.env -> bool
@@ -17,20 +17,8 @@ val ring_axioms  : EcEnv.env -> ring  -> (symbol * form) list
 val field_axioms : EcEnv.env -> field -> (symbol * form) list
 
 (* -------------------------------------------------------------------- *)
-val n_ring_congr : 
-  judgment_uc -> EcEnv.LDecl.hyps ->
-  cring -> RState.rstate ->
-  form -> int list -> form list ->
-    form * int * EcLogic.goals
+val t_ring : ring -> eqs -> form * form -> FApi.backward
+val t_ring_simplify : ring -> eqs -> form * form -> FApi.backward
 
-val n_ring_norm :
-  judgment_uc ->  EcEnv.LDecl.hyps ->
-  cring -> RState.rstate ->
-  form ->
-  RState.rstate * form * int * EcLogic.goals
-
-val t_ring : ring -> eqs -> form * form -> tactic
-val t_ring_simplify : ring -> eqs -> form * form -> tactic
-
-val t_field : field -> eqs -> form * form -> tactic
-val t_field_simplify : field -> eqs -> form * form -> tactic
+val t_field : field -> eqs -> form * form -> FApi.backward
+val t_field_simplify : field -> eqs -> form * form -> FApi.backward

src/ecBaseLogic.ml

@@ -1,5 +1,4 @@
 (* -------------------------------------------------------------------- *)
-open EcIdent
 open EcTypes
 open EcFol
 
@@ -57,42 +56,6 @@ type i_pat =
   | IPwhile of s_pat 
 and s_pat = (int (* index of targetted instr. *) * i_pat) list
 
-class virtual xrule (name : string) =
-object
-  method name = name
-end
-
-type rule =
-| RN_admit
-| RN_conv
-| RN_intro      of [`Raw of EcIdent.t list | `Exist]
-| RN_elim       of [`Exist]
-| RN_weak       of Sid.t
-| RN_apply
-| RN_smt
-| RN_revert
-| RN_hypothesis of EcIdent.t
-| RN_lemma      of EcPath.path * ty list
-| RN_xtd        of xrule
-
-type 'a rule_arg = 
-| RA_form of EcFol.form             (* formula             *)
-| RA_id   of EcIdent.t              (* local ident         *)
-| RA_mp   of EcPath.mpath           (* module              *)
-| RA_node of 'a                     (* sub-derivation      *)
-
-type 'a rnode = {
-  pr_name : rule;
-  pr_hyps : 'a rule_arg list
-}
-
-type l_decl = hyps * form
-
-type judgment = {
-  j_decl : l_decl;
-  j_rule : judgment rnode;
-}
-
 (* -------------------------------------------------------------------- *)
 type tac_error =
   | UnknownAx             of EcPath.path

src/ecBaseLogic.mli

@@ -41,42 +41,6 @@ type i_pat =
 (* the first pair value represents the number of instructions to skip *)
 and s_pat = (int * i_pat) list        
 
-class virtual xrule : string ->
-object
-  method name : string
-end
-
-type rule =
-| RN_admit
-| RN_conv
-| RN_intro      of [`Raw of EcIdent.t list | `Exist]
-| RN_elim       of [`Exist]
-| RN_weak       of Sid.t
-| RN_apply
-| RN_smt
-| RN_revert
-| RN_hypothesis of EcIdent.t
-| RN_lemma      of EcPath.path * ty list
-| RN_xtd        of xrule
-
-type 'a rule_arg = 
-| RA_form of EcFol.form             (* formula             *)
-| RA_id   of EcIdent.t              (* local ident         *)
-| RA_mp   of EcPath.mpath           (* module              *)
-| RA_node of 'a                     (* sub-derivation      *)
-
-type 'a rnode = {
-  pr_name : rule;
-  pr_hyps : 'a rule_arg list
-}
-
-type l_decl = hyps * form
-
-type judgment = {
-  j_decl : l_decl;
-  j_rule : judgment rnode;
-}
-
 (* -------------------------------------------------------------------- *)
 type tac_error =
   | UnknownAx             of EcPath.path

src/ecCommands.ml

@@ -3,7 +3,6 @@ open EcUtils
 open EcLocation
 open EcParsetree
 open EcTyping
-open EcLogic
 
 (* -------------------------------------------------------------------- *)
 type pragma = {
@@ -24,9 +23,12 @@ exception TopError of EcLocation.t * exn
 
 let rec toperror_of_exn ?gloc exn =
   match exn with
-  | TyError  (loc, _, _) -> Some (loc, exn)
+  | TyError  (loc, _, _)   -> Some (loc, exn)
   | EcBaseLogic.TacError _ -> Some (odfl _dummy gloc, exn)
-  | ParseError (loc, _)  -> Some (loc, exn)
+  | ParseError (loc, _)    -> Some (loc, exn)
+
+  | EcCoreGoal.TcError (_, _, _) ->
+      Some (odfl _dummy gloc, exn)
 
   | LocError (loc, e)    -> begin
       let gloc = if EcLocation.isdummy loc then gloc else Some loc in
@@ -275,7 +277,7 @@ and process_tactics (scope : EcScope.scope) t =
 
   match t with
   | `Actual t  -> EcScope.Tactics.process scope mode t
-  | `Proof  pm -> EcScope.Tactics.proof   scope mode pm.pm_strict pm.pm_newengine
+  | `Proof  pm -> EcScope.Tactics.proof   scope mode pm.pm_strict
 
 (* -------------------------------------------------------------------- *)
 and process_save (scope : EcScope.scope) loc =
@@ -455,19 +457,8 @@ let pp_current_goal stream =
       match puc.S.puc_jdg with
       | S.PSNoCheck -> ()
 
-      | S.PSCheck (juc, ns) -> begin
-        let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
-
-          match List.ohead ns with
-          | None   -> Format.fprintf stream "No more goals@\n%!"
-          | Some n ->
-            let hyps, concl = get_goal (juc, n) in
-            let g = EcEnv.LDecl.tohyps hyps, concl in
-              EcPrinting.pp_goal ppe stream (List.length ns, g)
-      end
-
-      | S.PSNewEngine pf -> begin
-        let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
+      | S.PSCheck pf -> begin
+          let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in
 
           match EcCoreGoal.opened pf with
           | None -> Format.fprintf stream "No more goals@\n%!"