From 1836052e4215c79479f616de6c71cf36f01c8216 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Jul 2009 22:05:07 +0000 Subject: [PATCH] Record fields declared as coercions as now really declared as coercions. --- .../grafite_engine/grafiteEngine.ml | 25 +++++++++++++------ 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5d1b81d74..be069fce1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -702,6 +702,12 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt = status, src, tgt, cpos, arity ;; +let basic_eval_and_inject_ncoercion infos status = + let status = basic_eval_ncoercion infos status in + let dump = inject_ncoercion infos::status#dump in + status#set_dump dump +;; + let eval_ncoercion status name t ty (id,src) tgt = let metasenv,subst,status,ty = @@ -714,12 +720,10 @@ let eval_ncoercion status name t ty (id,src) tgt = let t = NCicUntrusted.apply_subst subst [] t in let status, src, tgt, cpos, arity = - src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt + src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in + let status = + basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status in - - let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in - let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in - let status = status#set_dump dump in status,`New [] ;; @@ -1010,8 +1014,15 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = let status = List.fold_left (fun status (name,cpos,arity) -> - (*CSC: COME DICHIARO LA COERCION??? *) - status + let metasenv,subst,status,t = + GrafiteDisambiguate.disambiguate_nterm None status [] [] [] + ("",0,CicNotationPt.Ident (name,None)) in + assert (metasenv = [] && subst = []); + let ty = NCicTypeChecker.typeof ~subst ~metasenv [] t in + let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in +prerr_endline ("COERCION " ^ name ^ " cpos = " ^ string_of_int cpos ^ " arity = " ^ string_of_int arity); + basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) + status ) status coercions in status,uris -- 2.39.2