initial implementation of `ncoercion name : type := body on name : pat to pat`

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c0bfdb933aee59858b261f4d6f4d5884f55f9db2..c75e1aa3fa2ebe3549290262fb764349bc6244f2 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -495,6 +495,62 @@ let eval_unification_hint status t n =
   status,`New []
 ;;
 
+let basic_eval_ncoercion (name,t,s,d,p,a) status =
+  NCicCoercion.index_coercion status t s d a p
+;;
+
+let inject_ncoercion =
+ let basic_eval_ncoercion x ~refresh_uri_in_universe ~refresh_uri_in_term =
+  basic_eval_ncoercion x
+ in
+  NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
+;;
+
+let eval_ncoercion status name t ty (id,src) tgt = 
+
+ let metasenv,subst,status,ty =
+  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ assert (metasenv=[]);
+ let ty = NCicUntrusted.apply_subst subst [] ty in
+ let metasenv,subst,status,t =
+  GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst subst [] t in
+
+ let src, cpos = 
+   let rec aux cpos ctx = function
+     | NCic.Prod (name,ty,bo) ->
+        if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
+        else
+          let metasenv,subst,status,src =
+            GrafiteDisambiguate.disambiguate_nterm 
+              None status [] [] [] ("",0,src) in
+          let src = NCicUntrusted.apply_subst subst [] src in
+          let _ = NCicUnification.unify status metasenv subst ctx ty src in
+          src, cpos
+     | _ -> assert false
+   in
+     aux 0 [] ty
+ in
+ let tgt, arity = 
+   let metasenv,subst,status,tgt =
+     GrafiteDisambiguate.disambiguate_nterm 
+       None status [] [] [] ("",0,tgt) in
+   let tgt = NCicUntrusted.apply_subst subst [] tgt in
+   (* CHECK *)
+   let rec count_prod = function
+     | NCic.Prod (_,_,x) -> 1 + count_prod x
+     | _ -> 0
+   in
+    tgt, count_prod tgt
+ 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 []
+;;
+
 let basic_eval_add_constraint (s,u1,u2) status =
  NCicLibrary.add_constraint status s u1 u2
 ;;
@@ -700,6 +756,8 @@ let subst_metasenv_and_fix_names status =
 let rec eval_ncommand opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
+  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+      eval_ncoercion status name t ty source target
   | GrafiteAst.NQed loc ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")