From 72cd94b68037956a70b98cfa54f316fd54e52bae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jul 2009 21:53:50 +0000 Subject: [PATCH] initial implementation of `ncoercion name : type := body on name : pat to pat` --- .../software/components/grafite/grafiteAst.ml | 5 +- .../components/grafite/grafiteAstPp.ml | 1 + .../grafite_engine/grafiteEngine.ml | 58 +++++++++++++++++++ .../grafite_parser/grafiteParser.ml | 5 ++ .../components/ng_refiner/nCicCoercion.ml | 40 +++++++------ 5 files changed, 91 insertions(+), 18 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 14c487702..60e3aac4b 100644 --- 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 8fbe6b8d1..2cd7a4f4f 100644 --- 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 c0bfdb933..c75e1aa3f 100644 --- 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 d031bbad3..dfef4d237 100644 --- 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>; 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 29fe0fd54..31768a62d 100644 --- 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) ;; -- 2.39.2