diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-04 14:22:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-05 02:00:07 +0200 |
| commit | a51cce369b9c634a93120092d4c7685a242d55b1 (patch) | |
| tree | dd68ea8dadf86f9a6eb400839f515ed5b9cf8f95 /kernel/vconv.ml | |
| parent | 31c7542731a62f56bd60f443a84d68813f8780a8 (diff) | |
Fix handling of primitive projections in VM.
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
Diffstat (limited to 'kernel/vconv.ml')
| -rw-r--r-- | kernel/vconv.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 1c31cc041..a03a67db8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -18,8 +18,8 @@ let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2) | Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2) - | Zswitch _, Zswitch _ -> true - | _ , _ -> false + | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true + | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false let rec compare_stack stk1 stk2 = match stk1, stk2 with @@ -81,7 +81,10 @@ and conv_whd env pb k whd1 whd2 cu = conv_whd env pb k whd1 (force_whd v stk) cu | Vatom_stk(Aiddef(_,v),stk), _ -> conv_whd env pb k (force_whd v stk) whd2 cu - | _, _ -> raise NotConvertible + + | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible + and conv_atom env pb k a1 stk1 a2 stk2 cu = match a1, a2 with @@ -110,7 +113,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu | _, Aiddef(ik2,v2) -> conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu - | _, _ -> raise NotConvertible + | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = match stk1, stk2 with @@ -131,7 +134,11 @@ and conv_stack env k stk1 stk2 cu = done; conv_stack env k stk1 stk2 !rcu else raise NotConvertible - | _, _ -> raise NotConvertible + | Zproj p1 :: stk1, Zproj p2 :: stk2 -> + if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu + else raise NotConvertible + | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _ + | Zproj _ :: _, _ -> raise NotConvertible and conv_fun env pb k f1 f2 cu = if f1 == f2 then cu |