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 eb994854f49c6d0e648aa7c4fa916aad18a38b63..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
 ;;
@@ -625,7 +681,8 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let rec eval_ng_tac (text, prefix_len, tac) =
+let eval_ng_tac tac =
+ let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
@@ -677,8 +734,14 @@ let rec eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (eval_ng_tac (text, prefix_len, tac))
+      (aux f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
+  | GrafiteAst.NBlock (_,l) -> 
+      NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
+  |GrafiteAst.NRepeat (_,tac) ->
+      NTactics.repeat_tac (f f (text, prefix_len, tac))
+ in
+  aux aux tac (* trick for non uniform recursion call *)
 ;;
       
 let subst_metasenv_and_fix_names status =
@@ -693,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")