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

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 14c4877026b82615f5da807bb55f1f54b991ab3d..60e3aac4bfa0d2ad8ba476ecf1082c434cf22f1c 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -190,7 +190,7 @@ type ('term,'lazy_term) macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 25
+let magic = 26
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
@@ -214,6 +214,9 @@ type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
   | NUnivConstraint of loc * bool * NUri.uri * NUri.uri
+  | NCoercion of loc * string *
+      CicNotationPt.term * CicNotationPt.term *
+      (string * CicNotationPt.term) * CicNotationPt.term
   | NQed of loc
 
 type punctuation_tactical =

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 8fbe6b8d1c709b84dc995fd6bb020e3603346927..2cd7a4f4fcddfee286d115b84ff79c5a18cee9ad 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -360,6 +360,7 @@ let pp_ncommand = function
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
+  | NCoercion (_) -> "not supported"
   | NQed (_) -> "nqed"
     
 let pp_command ~term_pp ~obj_pp = function

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")

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index d031bbad3c59620d99f6ff8e2f2267a0c40ef7ca..dfef4d237a0ea34c8883b2b23b1e734fb46b8fcd 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -829,6 +829,11 @@ EXTEND
          G.NUnivConstraint (loc, strict,u1,u2)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         G.UnificationHint (loc, t, n)
+    | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term; 
+        SYMBOL <:unicode<def>>; t = term; "on"; 
+        id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
+        "to"; target = term ->
+          G.NCoercion(loc,name,t,ty,(id,source),target)     
     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields))
   ]];

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 29fe0fd540d48924dd06a8b52c319cc9497848bb..31768a62dd6ac11e474dca0c2ce997c24c422181 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -11,6 +11,9 @@
 
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
+let debug s = prerr_endline (Lazy.force s);;
+let debug _ = ();;
+
 module COT : Set.OrderedType with type t = NCic.term * int * int = 
   struct
         type t = NCic.term * int * int
@@ -39,12 +42,13 @@ class status =
 let index_coercion status c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
   let data = (c,arity,arg) in
-(*
-  prerr_endline ("INDEX:" ^ 
+
+  debug (lazy ("INDEX:" ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
-    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
-*)
+    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
+    string_of_int arg ^ " " ^ string_of_int arity));
+
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
   status#set_coerc_db (db_src, db_tgt)
@@ -69,15 +73,15 @@ let index_old_db odb (status : #status) =
                    NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
                  in
 (*
-            prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" 
+            debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" 
               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
 *)
                 src, tgt
               | t -> 
-                  prerr_endline (
-                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
+                  debug (lazy (
+                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
                   assert false
             in
             index_coercion status c src tgt arity arg
@@ -94,31 +98,33 @@ let look_for_coercion status metasenv subst context infty expty =
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
   | _ ->
-(*
-    prerr_endline ("LOOK FOR COERCIONS: " ^ 
+
+    debug (lazy ("LOOK FOR COERCIONS: " ^ 
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
-      NCicPp.ppterm ~metasenv ~subst ~context expty);
-*)
+      NCicPp.ppterm ~metasenv ~subst ~context expty));
+
     let set_src = DB.retrieve_unifiables db_src infty in
     let set_tgt = DB.retrieve_unifiables db_tgt expty in
     let candidates = CoercionSet.inter set_src set_tgt in
-(*
-    prerr_endline ("CANDIDATES: " ^ 
+
+    debug (lazy ("CANDIDATES: " ^ 
       String.concat "," (List.map (fun (t,_,_) ->
         NCicPp.ppterm ~metasenv ~subst ~context t) 
-      (CoercionSet.elements candidates)));
-*)
+      (CoercionSet.elements candidates))));
+
     List.map
       (fun (t,arity,arg) ->
           let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
           let ty, metasenv, args = 
            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
           in
-  (*       prerr_endline (
+
+          debug (lazy (
             NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
             NCicPp.ppterm ~metasenv ~subst ~context
             (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
-              string_of_int (List.length args) ^ " == " ^ string_of_int arg); *)
+              string_of_int (List.length args) ^ " == " ^ string_of_int arg)); 
+             
           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
       (CoercionSet.elements candidates)
 ;;