Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit fc0962a0 authored by MARCHE Claude's avatar MARCHE Claude

Fix some bugs in Ocaml extraction related to ghost parameters

parent a19693df
......@@ -20,6 +20,8 @@ ifeq ($(BENCH),yes)
endif
MLWUTIL=Nat
MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
......@@ -28,9 +30,10 @@ MLWTYPES=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
MLWIMPL=$(MLWTYPES) ProverMain ProverTest
BD=build
MLUTIL=$(patsubst %,$(BD)/%__Nat,$(MLWUTIL))
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLWTYPES))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLWIMPL))
MLALL=$(MLTYPES) $(MLIMPL)
MLALL=$(MLUTIL) $(MLTYPES) $(MLIMPL)
ML=$(patsubst %,%.ml,$(MLALL))
CMX=$(patsubst %,%.cmx,$(MLALL))
OCAMLC=ocamlopt.opt
......
......@@ -307,8 +307,8 @@ module Impl
&& eval rho.unifier y = Var_fo_term y
&& st tm rho.unifier = Var_fo_term y
&& is_fo_term_free_var_in_fo_term y (st tm rho.unifier)) && y >= 0 } ;
let by = BA.get rhob y in
match by with
let by' = BA.get rhob y in
match by' with
| Nil -> bottomvar rhob rho y ;
if x = y
then raise UnificationFailure
......@@ -902,18 +902,18 @@ module Impl
assert { st bxm rhoi' = sc rhobm rhoi' x
= rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
res
| _ -> let by = BA.get rhob y in
match by with
| Cons (Assign by) _ -> (*checkit rho y it2 ;*)
let bym = by.model_fo_term_field in
| _ -> let by' = BA.get rhob y in
match by' with
| Cons (Assign by') _ -> (*checkit rho y it2 ;*)
let bym = by'.model_fo_term_field in
let rhobm = rho.unifier_base_model in
let rhoi = rho.unifier in
assert { sdata_inv (Assign by) } ;
assert { sdata_inv (Assign by') } ;
assert { bym = rhobm y (*/\ mem y fv*) } ;
assert { st bym rhoi = sc rhobm rhoi y = rhoi y = st t2m rhoi
&& forall s:func int (fo_term int int).
st bym (sc rhoi s) = st t2m (sc rhoi s) } ;
let res = unification_term t1 by lv rhob rho lp (*fv s it1 (it2-1)*) in
let res = unification_term t1 by' lv rhob rho lp (*fv s it1 (it2-1)*) in
let rhoi' = res.final_unifier.unifier in
assert { st bym rhoi' = sc rhobm rhoi' y
= rhoi' y = st t2m rhoi' && st bym rhoi' = st t2m rhoi' } ;
......
......@@ -168,6 +168,8 @@ module Translate = struct
open Decl
let type_unit = ML.Ttuple []
let rec type_ info ty = match ty.ty_node with
| Tyvar v ->
ML.Tvar v.tv_name
......@@ -458,7 +460,10 @@ module Translate = struct
| _ -> assert false
let pv_name pv = pv.pv_vs.vs_name
let pvty info pv = vsty info pv.pv_vs
let pvty info pv =
if pv.pv_ghost then (pv.pv_vs.vs_name, type_unit)
else vsty info pv.pv_vs
let lv_name = function
| LetV pv -> pv_name pv
......@@ -473,12 +478,20 @@ module Translate = struct
| _ -> true
let filter_ghost_params =
(* removal of ghost does not work
let dummy = create_pvsymbol (Ident.id_fresh "") ity_unit in
fun args ->
match List.filter (fun v -> not v.Mlw_ty.pv_ghost) args with
| [] -> [dummy]
| l -> l
*)
fun args -> args (* filtering ghost happens in pvty *)
(*
List.map
(fun v -> if v.Mlw_ty.pv_ghost then
create_pvsymbol (Ident.id_fresh "") ity_unit
else v)
*)
let rec expr info e =
assert (not e.e_ghost);
match e.e_node with
......@@ -499,6 +512,7 @@ module Translate = struct
let n = Number.compute_int (get_int_constant e1) in
let e1 = ML.Esyntax (BigInt.to_string n, []) in
ML.Esyntax (s, [e1])
(*
| Eapp (e, v, _) when v.pv_ghost ->
(* ghost parameters are ignored *)
begin
......@@ -506,10 +520,13 @@ module Translate = struct
| Eapp _ -> expr info e
| _ -> ML.Eapp (expr info e, [ML.enop])
end
*)
| Eapp (e, v, _) ->
ML.Eapp (expr info e, [ML.Eident (pv_name v)])
| Elet ({ let_expr = e1 }, e2) when e1.e_ghost ->
expr info e2
| Elet ({ let_sym = lv; let_expr = e1 }, e2) when e1.e_ghost ->
(* TODO: remove superflous let *)
ML.Elet (lv_name lv, ML.enop, expr info e2)
| Elet ({ let_sym = LetV pv }, e2) when ity_equal pv.pv_ity ity_mark ->
expr info e2
| Elet ({ let_sym = LetV pv; let_expr = e1 }, e2) when is_underscore pv ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment