From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- plugins/firstorder/unify.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d9ab36ad64..01c0197443 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -21,7 +21,10 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) +let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) + let unif t1 t2= + let evd = Evd.empty in (** FIXME *) let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -47,18 +50,18 @@ let unif t1 t2= else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- plugins/firstorder/unify.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 01c0197443..fb237f29bf 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -41,8 +41,8 @@ let unif t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta Evd.empty t1) - and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in + let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1)) + and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in match (kind_of_term nt1),(kind_of_term nt2) with Meta i,Meta j-> if not (Int.equal i j) then -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- plugins/firstorder/unify.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index fb237f29bf..205cb282d1 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -21,7 +21,8 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) -let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) +let strip_outer_cast t = + EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) let unif t1 t2= let evd = Evd.empty in (** FIXME *) -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- plugins/firstorder/unify.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 205cb282d1..5520c7e35d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -42,8 +42,8 @@ let unif t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1)) - and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in + let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1))) + and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in match (kind_of_term nt1),(kind_of_term nt2) with Meta i,Meta j-> if not (Int.equal i j) then -- cgit v1.2.3 From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- plugins/firstorder/unify.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder/unify.ml') diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 5520c7e35d..7cbfb8e7de 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -24,6 +24,8 @@ exception UFAIL of constr*constr let strip_outer_cast t = EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) +let pop t = Vars.lift (-1) t + let unif t1 t2= let evd = Evd.empty in (** FIXME *) let bige=Queue.create () @@ -62,7 +64,7 @@ let unif t1 t2= | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige + Queue.add (a,c) bige;Queue.add (pop b,pop d) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; -- cgit v1.2.3