From 2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Sep 2006 15:51:36 +0000 Subject: [PATCH] BIG FAT COMMIT REGARDING COERCIONS: - multiple coercions from the same type - coercions to funclass - fixed cicPp for letin and pi - improved coercions ma with a minimal test for funclass - cheanged XML and Ast to support `Coercion ARITY label - added syntax: coercion URI ARITY recordfield :ARITY> type - added topological sorting module (funcotr) in extlib - abstracted graphviz to allow non strict and tred graphs - tentative (not yet properly done) of hiding coercions in content - fixed a problem in metadata contraints iof there are no constraints - renamed/moved/commented some functions (eat_prod related) in the refiner - crossed fingers --- components/acic_content/cicNotationPp.ml | 7 +- components/acic_content/cicNotationPt.ml | 2 +- components/acic_content/cicNotationUtil.ml | 2 +- components/acic_content/termAcicContent.ml | 33 +- components/cic/cic.ml | 7 +- components/cic/cicParser.ml | 19 +- components/cic/cicUtil.ml | 11 + components/cic/cicUtil.mli | 1 + components/cic_acic/cic2Xml.ml | 11 +- components/cic_acic/cic2acic.ml | 4 +- components/cic_disambiguation/disambiguate.ml | 8 +- components/cic_proof_checking/cicPp.ml | 8 +- components/cic_unification/cicRefine.ml | 557 +++++++++++------- components/cic_unification/cicUnification.ml | 17 +- components/extlib/.depend | 4 + components/extlib/Makefile | 1 + components/extlib/graphvizPp.ml | 5 +- components/extlib/graphvizPp.mli | 3 + components/extlib/hExtlib.ml | 5 + components/extlib/hExtlib.mli | 1 + components/extlib/hTopoSort.ml | 69 +++ components/extlib/hTopoSort.mli | 32 + components/grafite/grafiteAst.ml | 4 +- components/grafite/grafiteAstPp.ml | 6 +- components/grafite/grafiteMarshal.ml | 4 +- components/grafite_engine/grafiteEngine.ml | 44 +- components/grafite_engine/grafiteSync.ml | 5 +- components/grafite_engine/grafiteSync.mli | 2 +- components/grafite_parser/grafiteParser.ml | 15 +- components/lexicon/lexiconAst.ml | 2 +- components/library/cicCoercion.ml | 174 ++++-- components/library/coercDb.ml | 58 +- components/library/coercDb.mli | 2 + components/library/coercGraph.ml | 41 +- components/library/coercGraph.mli | 11 +- components/library/librarySync.ml | 51 +- components/library/librarySync.mli | 2 +- components/metadata/metadataConstraints.ml | 24 +- components/metadata/metadataDeps.ml | 2 +- components/tactics/primitiveTactics.ml | 11 +- components/tactics/tactics.mli | 2 +- matita/lablGraphviz.ml | 25 +- matita/lablGraphviz.mli | 15 +- matita/library/legacy/coq.ma | 23 +- matita/library/logic/equality.ma | 21 +- matita/matitaMathView.ml | 4 +- matita/tests/coercions.ma | 50 +- 47 files changed, 982 insertions(+), 423 deletions(-) create mode 100644 components/extlib/hTopoSort.ml create mode 100644 components/extlib/hTopoSort.mli diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml index cdc0946e6..49cefaec7 100644 --- a/components/acic_content/cicNotationPp.ml +++ b/components/acic_content/cicNotationPp.ml @@ -289,8 +289,11 @@ let pp_fields fields = (if fields <> [] then "\n" else "") ^ String.concat ";\n" (List.map - (fun (name,ty,coercion) -> - " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields) + (fun (name,ty,coercion,arity) -> + " " ^ name ^ + if coercion then (":" ^ + if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^ + pp_term ty) fields) let pp_obj = function | Ast.Inductive (params, types) -> diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml index 609fb9d2f..6ea1ec917 100644 --- a/components/acic_content/cicNotationPt.ml +++ b/components/acic_content/cicNotationPt.ml @@ -174,7 +174,7 @@ type obj = * will be given in proof editing mode using the tactical language, * unless the flavour is an Axiom *) - | Record of (string * term) list * string * term * (string * term * bool) list + | Record of (string * term) list * string * term * (string * term * bool * int) list (** left parameters, name, type, fields *) (** {2 Standard precedences} *) diff --git a/components/acic_content/cicNotationUtil.ml b/components/acic_content/cicNotationUtil.ml index 8e487ed11..d9114b180 100644 --- a/components/acic_content/cicNotationUtil.ml +++ b/components/acic_content/cicNotationUtil.ml @@ -366,7 +366,7 @@ let freshen_obj obj = let index = ref 0 in let freshen_term = freshen_term ~index in let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in - let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in + let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in match obj with | CicNotationPt.Inductive (params, indtypes) -> let indtypes = diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml index 7948f2654..516d5f542 100644 --- a/components/acic_content/termAcicContent.ml +++ b/components/acic_content/termAcicContent.ml @@ -121,16 +121,31 @@ let ast_of_acic0 term_info acic k = | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args)) | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) -> - if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && - !Acic2content.hide_coercions + let last_n n l = + let rec aux = + function + [] -> assert false + | [_] as l -> l,1 + | he::tl -> + let (res,len) as res' = aux tl in + if len < n then + he::res,len + 1 + else + res' + in + match fst (aux l) with + [] -> assert false + | [t] -> t + | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> + idref aid (Ast.Appl (l@tl)) + | l -> idref aid (Ast.Appl l) + in + let deannot_he = Deannotate.deannotate_term he in + if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions then - let rec last = - function - [] -> assert false - | [t] -> t - | _::tl -> last tl - in - idref aid (k (last tl)) + match CoercGraph.is_a_coercion_to_funclass deannot_he with + | None -> idref aid (last_n 1 (List.map k tl)) + | Some i -> idref aid (last_n (i+1) (List.map k tl)) else idref aid (Ast.Appl (List.map k args)) | Cic.AAppl (aid,args) -> diff --git a/components/cic/cic.ml b/components/cic/cic.ml index 20a6cb457..549587215 100644 --- a/components/cic/cic.ml +++ b/components/cic/cic.ml @@ -66,12 +66,13 @@ type object_flavour = ] type object_class = - [ `Coercion + [ `Coercion of int | `Elim of sort (** elimination principle; if sort is Type, the universe is * not relevant *) - | `Record of (string * bool) list (** + | `Record of (string * bool * int) list (** inductive type that encodes a record; the arguments are - the record fields names and if they are coercions *) + the record fields names and if they are coercions and + then the coercion arity *) | `Projection (** record projection *) ] diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml index 1e9a3a33c..150fe4ad9 100644 --- a/components/cic/cicParser.ml +++ b/components/cic/cicParser.ml @@ -678,7 +678,13 @@ let end_element ctxt tag = let class_modifiers = pop_class_modifiers ctxt in push ctxt (match pop_tag_attrs ctxt with - | ["value", "coercion"] -> Obj_class `Coercion + | ["value", "coercion"] -> Obj_class (`Coercion 0) + | ("value", "coercion")::["arity",n] + | ("arity",n)::["value", "coercion"] -> + let arity = try int_of_string n with Failure _ -> + parse_error "\"arity\" must be an integer" + in + Obj_class (`Coercion arity) | ["value", "elim"] -> (match class_modifiers with | [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort) @@ -691,8 +697,15 @@ let end_element ctxt tag = (function | Obj_field name -> (match Str.split (Str.regexp " ") name with - | [name] -> name, false - | [name;"coercion"] -> name,true + | [name] -> name, false, 0 + | [name;"coercion"] -> name,true,0 + | [name;"coercion"; n] -> + let n = + try int_of_string n + with Failure _ -> + parse_error "int expected after \"coercion\"" + in + name,true,n | _ -> parse_error "wrong \"field\"'s name attribute") diff --git a/components/cic/cicUtil.ml b/components/cic/cicUtil.ml index de796910a..6e07a4995 100644 --- a/components/cic/cicUtil.ml +++ b/components/cic/cicUtil.ml @@ -207,6 +207,17 @@ let attributes_of_obj = function | Cic.CurrentProof (_, _, _, _, _, attributes) | Cic.InductiveDefinition (_, _, _, attributes) -> attributes + +let arity_of_composed_coercion obj = + let attrs = attributes_of_obj obj in + try + let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in + match tag with + | `Class (`Coercion n) -> n + | _-> assert false + with Not_found -> 0 +;; + let rec mk_rels howmany from = match howmany with | 0 -> [] diff --git a/components/cic/cicUtil.mli b/components/cic/cicUtil.mli index b8d71f51f..422bb130b 100644 --- a/components/cic/cicUtil.mli +++ b/components/cic/cicUtil.mli @@ -53,6 +53,7 @@ val id_of_annterm: Cic.annterm -> Cic.id val params_of_obj: Cic.obj -> UriManager.uri list val attributes_of_obj: Cic.obj -> Cic.attribute list +val arity_of_composed_coercion: Cic.obj -> int (** mk_rels [howmany] [from] * creates a list of [howmany] rels starting from [from] in decreasing order *) diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml index 95f92346b..31765f055 100644 --- a/components/cic_acic/cic2Xml.ml +++ b/components/cic_acic/cic2Xml.ml @@ -269,7 +269,8 @@ let print_term ?ids_to_inner_sorts = let xml_of_attrs attributes = let class_of = function - | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"] + | `Coercion n -> + Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n] | `Elim s -> Xml.xml_nempty "class" [None,"value","elim"] [< Xml.xml_empty @@ -279,9 +280,13 @@ let xml_of_attrs attributes = | `Record field_names -> Xml.xml_nempty "class" [None,"value","record"] (List.fold_right - (fun (name,coercion) res -> + (fun (name,coercion,arity) res -> [< Xml.xml_empty "field" - [None,"name",if coercion then name ^ " coercion" else name]; + [None,"name", + if coercion then + name ^ " coercion " ^ string_of_int arity + else + name]; res >] ) field_names [<>]) | `Projection -> Xml.xml_empty "class" [None,"value","projection"] diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml index 6da648453..6cb2ad9a2 100644 --- a/components/cic_acic/cic2acic.ml +++ b/components/cic_acic/cic2acic.ml @@ -499,7 +499,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = let aobj = match obj with C.Constant (id,Some bo,ty,params,attrs) -> - let bo' = eta_fix [] [] bo in + let bo' = (*eta_fix [] []*) bo in let ty' = eta_fix [] [] ty in let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in @@ -557,7 +557,7 @@ let acic_object_of_cic_object ?(eta_fix=false) obj = (cid,i,acanonical_context,aterm)) conjectures' in (* let time1 = Sys.time () in *) - let bo' = eta_fix conjectures' [] bo in + let bo' = (*eta_fix conjectures' []*) bo in let ty' = eta_fix conjectures' [] ty in (* let time2 = Sys.time () in diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index cb4d85cfd..fbe191416 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -483,7 +483,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = let fields' = snd ( List.fold_left - (fun (context,res) (name,ty,_coercion) -> + (fun (context,res) (name,ty,_coercion,arity) -> let context' = Cic.Name name :: context in context',(name,interpretate_term context env None false ty)::res ) (context,[]) fields) in @@ -500,7 +500,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = concl fields' in let con' = add_params con in let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map (fun (x,_,y) -> x,y) fields in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) | CicNotationPt.Theorem (flavour, name, ty, bo) -> @@ -692,7 +692,7 @@ let domain_of_obj ~context ast = | CicNotationPt.Record (params,_,ty,fields) -> let dom = List.flatten - (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in + (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in let dom = List.fold_left (fun dom (_,ty) -> @@ -702,7 +702,7 @@ let domain_of_obj ~context ast = List.filter (fun (_,name) -> not ( List.exists (fun (name',_) -> name = Id name') params - || List.exists (fun (name',_,_) -> name = Id name') fields) + || List.exists (fun (name',_,_,_) -> name = Id name') fields) ) dom in rev_uniq domain_rev diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml index feca7c3cf..06bb082b4 100644 --- a/components/cic_proof_checking/cicPp.ml +++ b/components/cic_proof_checking/cicPp.ml @@ -80,10 +80,8 @@ let rec pp t l = UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l | C.Meta (n,l1) -> "?" ^ (string_of_int n) ^ "[" ^ -(* String.concat " ; " (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ -*) "]" | C.Sort s -> (match s with @@ -97,14 +95,14 @@ let rec pp t l = | C.Implicit _ -> "?" | C.Prod (b,s,t) -> (match b with - C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) - | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" + C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")" + | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")" ) | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")" | C.Lambda (b,s,t) -> "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")" | C.LetIn (b,s,t) -> - "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l) | C.Appl li -> "(" ^ (List.fold_right diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 48ae522f4..798c38540 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -32,8 +32,10 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; let insert_coercions = ref true +let pack_coercions = ref true let debug_print = fun _ -> () +(* let debug_print x = prerr_endline (Lazy.force x);; *) let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" @@ -123,24 +125,76 @@ let exp_impl metasenv subst context = let is_a_double_coercion t = let last_of l = - let rec aux = function - | x::[] -> x - | x::tl -> aux tl + let rec aux acc = function + | x::[] -> acc,x + | x::tl -> aux (acc@[x]) tl | [] -> assert false in - aux l - in - let dummyres = - false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None + aux [] l in + let imp = Cic.Implicit None in + let dummyres = false,imp, imp,imp,imp in match t with | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> (match last_of tl with - | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> - let head = last_of tl2 in - true, c1, c2, head + | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + let sib2,head = last_of tl2 in + true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl + (c2::sib2@[Cic.Implicit None])]) | _ -> dummyres) | _ -> dummyres + +let more_args_than_expected subst he context hetype' tlbody_and_type = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst he context ^ + " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^ + ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected") +;; + +let mk_prod_of_metas metasenv context' subst args = + let rec mk_prod metasenv context' = function + | [] -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + metasenv,Cic.Meta (idx, irl) + | (_,argty)::tl -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context' + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context' + in + let meta = Cic.Meta (idx,irl) in + let name = + (* The name must be fresh for context. *) + (* Nevertheless, argty is well-typed only in context. *) + (* Thus I generate a name (name_hint) in context and *) + (* then I generate a name --- using the hint name_hint *) + (* --- that is fresh in context'. *) + let name_hint = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context') + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) + in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context' name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = + mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl + in + metasenv,Cic.Prod (name,meta,target) + in + mk_prod metasenv context' args +;; let rec type_of_constant uri ugraph = let module C = Cic in @@ -526,20 +580,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t type_of_aux subst metasenv context he ugraph in let tlbody_and_type,subst'',metasenv'',ugraph2 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) tl ([],subst',metasenv',ugraph1) + typeof_list subst' metasenv' context ugraph1 tl in - let tl',applty,subst''',metasenv''',ugraph3 = + let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 = eat_prods true subst'' metasenv'' context he' hetype tlbody_and_type ugraph2 in - avoid_double_coercion context - subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty + let newappl = (C.Appl (coerced_he::coerced_args)) in + avoid_double_coercion + context subst''' metasenv''' ugraph3 newappl applty | C.Appl _ -> assert false | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -816,15 +865,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t subst,metasenv,ugraph) | _ -> (* easy case *) let tlbody_and_type,subst,metasenv,ugraph4 = - List.fold_right - (fun x (res,subst,metasenv,ugraph) -> - let x',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context x ugraph - in - (x', ty)::res,subst',metasenv',ugraph1 - ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + typeof_list subst metasenv context ugraph4 (right_args @ [term']) in - let _,_,subst,metasenv,ugraph4 = + let _,_,_,subst,metasenv,ugraph4 = eat_prods false subst metasenv context outtype outtypety tlbody_and_type ugraph4 in @@ -1126,7 +1169,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicPp.ppterm t2'')))) and avoid_double_coercion context subst metasenv ugraph t ty = - let b, c1, c2, head = is_a_double_coercion t in + let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in if b then let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in @@ -1135,207 +1178,326 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (fun c -> + (function + | c when not (CoercGraph.is_composite c) -> + debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); + None + | c -> let newt = match c with | Cic.Appl l -> Cic.Appl (l @ [head]) | _ -> Cic.Appl [c;head] in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); (try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in debug_print (lazy ("packing: " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + debug_print (lazy "tipa..."); + let subst, metasenv, ugraph = + (* COME MAI C'ERA UN IF su !pack_coercions ??? *) + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print (lazy "unifica..."); Some (newt, ty, subst, metasenv, ugraph) - with RefineFailure _ | Uncertain _ -> None)) + with + | RefineFailure s | Uncertain s when not !pack_coercions-> + debug_print s; debug_print (lazy "stop\n");None + | RefineFailure s | Uncertain s -> + debug_print s;debug_print (lazy "goon\n"); + try + pack_coercions := false; (* to avoid diverging *) + let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = + type_of_aux subst metasenv context c1_c2_implicit ugraph + in + pack_coercions := true; + let b, _, _, _, _ = + is_a_double_coercion refined_c1_c2_implicit + in + if b then + None + else + let head' = + match refined_c1_c2_implicit with + | Cic.Appl l -> HExtlib.list_last l + | _ -> assert false + in + let subst, metasenv, ugraph = + try fo_unif_subst subst context metasenv + head head' ugraph + with RefineFailure s| Uncertain s-> + debug_print s;assert false + in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv + refined_c1_c2_implicit t ugraph + in + Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph) + with + | RefineFailure s | Uncertain s -> + pack_coercions := true;debug_print s;None + | exn -> pack_coercions := true; raise exn)) candidates in (match selected with | Some x -> x | None -> - prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t); - assert false) + debug_print + (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); + t, ty, subst, metasenv, ugraph) | _ -> assert false) (* the composite coercion must exist *) else t, ty, subst, metasenv, ugraph + and typeof_list subst metasenv context ugraph l = + let tlbody_and_type,subst,metasenv,ugraph = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) l ([],subst,metasenv,ugraph) + in + tlbody_and_type,subst,metasenv,ugraph + and eat_prods - allow_coercions subst metasenv context he hetype tlbody_and_type ugraph + allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = - let rec mk_prod metasenv context' = - function - [] -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' - in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' - in - let meta = Cic.Meta (idx,irl) in - let name = - (* The name must be fresh for context. *) - (* Nevertheless, argty is well-typed only in context. *) - (* Thus I generate a name (name_hint) in context and *) - (* then I generate a name --- using the hint name_hint *) - (* --- that is fresh in context'. *) - let name_hint = - (* Cic.Name "pippo" *) - FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - ~typ:(CicMetaSubst.apply_subst subst argty) - in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) - FreshNamesGenerator.mk_fresh_name ~subst - [] context' name_hint ~typ:(Cic.Sort Cic.Prop) - in - let metasenv,target = - mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl - in - metasenv,Cic.Prod (name,meta,target) - in - let ((subst,metasenv,ugraph1),hetype') = - if CicUtil.is_meta_closed hetype then - (subst,metasenv,ugraph),hetype - else - let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in - try - fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype' - with exn -> - enrich localization_tbl he - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he - context ^ " (that has type " ^ - CicMetaSubst.ppterm_in_context subst hetype - context ^ ") is here applied to " ^ - string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected" - (* "\nReason: " ^ Lazy.force exn*)))) exn + (* aux function to add coercions to funclass *) + let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph = + (* {{{ body *) + let pristinemenv = metasenv in + let metasenv,hetype' = + mk_prod_of_metas metasenv context subst args_bo_and_ty + in + try + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods + subst context metasenv hetype hetype' ugraph + in + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + with RefineFailure s | Uncertain s as exn + when allow_coercions && !insert_coercions -> + (* {{{ we search a coercion of the head (saturated) to funclass *) + let metasenv = pristinemenv in + debug_print (lazy + ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ + " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^ + " cause: " ^ Lazy.force s)); + let how_many_args_are_needed = + let rec aux n = function + | Cic.Prod(_,_,t) -> aux (n+1) t + | _ -> n + in + aux 0 (CicMetaSubst.apply_subst subst hetype) + in + let args, remainder = + HExtlib.split_nth how_many_args_are_needed args_bo_and_ty + in + let args = List.map fst args in + let x = + if args <> [] then + match he with + | Cic.Appl l -> Cic.Appl (l@args) + | _ -> Cic.Appl (he::args) + else + he + in + let x,xty,subst,metasenv,ugraph = + type_of_aux subst metasenv context x ugraph + in + let carr_src = + CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) + in + let carr_tgt = CoercDb.Fun 0 in + match CoercGraph.look_for_coercion' carr_src carr_tgt with + | CoercGraph.NoCoercion + | CoercGraph.NotMetaClosed + | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercion candidates -> + match + HExtlib.list_findopt + (fun coerc -> + let t = Cic.Appl [coerc;x] in + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + try + (* we want this to be available in the error handler fo the + * following (so it has its own try. *) + let t,tty,subst,metasenv,ugraph = + type_of_aux subst metasenv context t ugraph + in + try + let metasenv, hetype' = + mk_prod_of_metas metasenv context subst remainder + in + debug_print (lazy + (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ + CicMetaSubst.ppterm subst hetype')); + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods + subst context metasenv tty hetype' ugraph + in + debug_print (lazy " success!"); + Some (subst,metasenv,ugraph,tty,t,remainder) + with + | Uncertain _ | RefineFailure _ + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> + try + let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = + fix_arity + metasenv context subst t tty remainder ugraph + in + Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) + with exn -> None + with exn -> None) + candidates + with + | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + | None -> + enrich localization_tbl he + ~f:(fun _-> more_args_than_expected subst he context hetype + args_bo_and_ty) exn + (* }}} end coercion to funclass stuff *) + (* }}} end fix_arity *) in - let rec eat_prods metasenv subst context hetype ugraph = + (* aux function to process the type of the head and the args in parallel *) + let rec eat_prods_and_args + pristinemenv metasenv subst context he hetype ugraph newargs + = + (* {{{ body *) function - | [] -> [],metasenv,subst,hetype,ugraph + | [] -> newargs,subst,metasenv,he,hetype,ugraph | (hete, hety)::tl -> - (match (CicReduction.whd ~subst context hetype) with - Cic.Prod (n,s,t) -> - let arg,subst,metasenv,ugraph1 = - try - let subst,metasenv,ugraph1 = - fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph - in - hete,subst,metasenv,ugraph1 - with exn when allow_coercions && !insert_coercions -> - (* we search a coercion from hety to s *) - let coer, tgt_carr = - let carr t subst context = - CicReduction.whd ~delta:false - context (CicMetaSubst.apply_subst subst t ) - in - let c_hety = carr hety subst context in - let c_s = carr s subst context in - CoercGraph.look_for_coercion c_hety c_s, c_s - in - (match coer with - | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> - enrich localization_tbl hete - (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.NotMetaClosed -> - enrich localization_tbl hete - (Uncertain - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) - | CoercGraph.SomeCoercion candidates -> - let selected = - HExtlib.list_findopt - (fun c -> - try - let t = Cic.Appl[c;hete] in - let newt,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context - t ugraph - in - let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv - ugraph newt tgt_carr - in - let subst,metasenv,ugraph1 = - fo_unif_subst subst context metasenv - newhety s ugraph - in - Some (newt, subst, metasenv, ugraph) - with Uncertain _ | RefineFailure _ -> None) - candidates - in - (match selected with - | Some x -> x - | None -> - enrich localization_tbl hete - ~f:(fun _ -> - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete - context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety - context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn)) - | exn -> + match (CicReduction.whd ~subst context hetype) with + | Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph1 = + try + let subst,metasenv,ugraph1 = + fo_unif_subst_eat_prods2 + subst context metasenv hety s ugraph + in + (hete,hety),subst,metasenv,ugraph1 + (* {{{ we search a coercion from hety to s if fails *) + with RefineFailure _ | Uncertain _ as exn + when allow_coercions && !insert_coercions -> + let coer, tgt_carr = + let carr t subst context = + CicReduction.whd ~delta:false + context (CicMetaSubst.apply_subst subst t ) + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s, c_s + in + (match coer with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> enrich localization_tbl hete - ~f:(fun _ -> + (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst hety context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst s context - (* "\nReason: " ^ Lazy.force e*)))) exn - in - let coerced_args,metasenv',subst',t',ugraph2 = - eat_prods metasenv subst context - (CicSubstitution.subst arg t) ugraph1 tl - in - arg::coerced_args,metasenv',subst',t',ugraph2 - | _ -> - raise (RefineFailure - (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he - context ^ " (that has type " ^ - CicMetaSubst.ppterm_in_context subst hetype' - context ^ ") is here applied to " ^ - string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected")))) + (* "\nReason: " ^ Lazy.force e*)))) + | CoercGraph.NotMetaClosed -> + enrich localization_tbl hete + (Uncertain + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (fun c -> + try + let t = Cic.Appl[c;hete] in + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context + t ugraph + in + let newt, newty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv + ugraph newt tgt_carr + in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety s ugraph + in + Some ((newt,newty), subst, metasenv, ugraph) + with Uncertain _ | RefineFailure _ -> None) + candidates + in + (match selected with + | Some x -> x + | None -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) exn)) + | exn -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context ^ + "\nReason: " ^ Printexc.to_string exn))) exn + (* }}} end coercion stuff *) + in + eat_prods_and_args pristinemenv metasenv subst context he + (CicSubstitution.subst (fst arg) t) + ugraph1 (newargs@[arg]) tl + | _ -> + try + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + fix_arity + pristinemenv context subst he hetype + (newargs@[hete,hety]@tl) ugraph + in + eat_prods_and_args metasenv + metasenv subst context he hetype' ugraph [] args_bo_and_ty + with RefineFailure s | Uncertain s -> + (* unable to fix arity *) + let msg = + more_args_than_expected + subst he context hetype args_bo_and_ty + in + raise (RefineFailure msg) + (* }}} *) + in + (* first we check if we are in the simple case of a meta closed term *) + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + if CicUtil.is_meta_closed hetype then + (* this optimization is to postpone fix_arity (the most common case)*) + subst,metasenv,ugraph,hetype,he,args_bo_and_ty + else + (* this (says CSC) is also useful to infer dependent types *) + fix_arity metasenv context subst he hetype args_bo_and_ty ugraph in - let coerced_args,metasenv,subst,t,ugraph2 = - eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type + let coerced_args,subst,metasenv,he,t,ugraph = + eat_prods_and_args + metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty in - coerced_args,t,subst,metasenv,ugraph2 + he,(List.map fst coerced_args),t,subst,metasenv,ugraph in (* eat prods ends here! *) @@ -1566,7 +1728,7 @@ let pack_coercion metasenv ctx t = | C.Appl l -> let l = List.map (merge_coercions ctx) l in let t = C.Appl l in - let b,_,_,_ = is_a_double_coercion t in + let b,_,_,_,_ = is_a_double_coercion t in (* prerr_endline "CANDIDATO!!!!"; *) if b then let ugraph = CicUniv.empty_ugraph in @@ -1721,3 +1883,4 @@ let typecheck ~localization_tbl metasenv uri obj = profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj let _ = DoubleTypeInference.pack_coercion := pack_coercion;; +(* vim:set foldmethod=marker: *) diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 44712199e..ecde4cdfd 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -578,13 +578,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_l test_equality_only subst metasenv (lr1, lr2) ugraph with - | UnificationFailure _ - | Uncertain _ as exn -> + | UnificationFailure s + | Uncertain s as exn -> (match l1, l2 with | (((Cic.Const (uri1, ens1)) as c1) :: tl1), (((Cic.Const (uri2, ens2)) as c2) :: tl2) when CoercGraph.is_a_coercion c1 && - CoercGraph.is_a_coercion c2 -> + CoercGraph.is_a_coercion c2 && + not (UriManager.eq uri1 uri2) -> let body1, attrs1, ugraph = match CicEnvironment.get_obj ugraph uri1 with | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u @@ -596,9 +597,15 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ | _ -> assert false in let is_composite1 = - List.exists ((=) (`Class `Coercion)) attrs1 in + List.exists + (function `Class (`Coercion _) -> true | _-> false) + attrs1 + in let is_composite2 = - List.exists ((=) (`Class `Coercion)) attrs2 in + List.exists + (function `Class (`Coercion _) -> true | _-> false) + attrs2 + in (match is_composite1, is_composite2 with | false, false -> raise exn | true, false -> diff --git a/components/extlib/.depend b/components/extlib/.depend index bd82a603c..c076e9f96 100644 --- a/components/extlib/.depend +++ b/components/extlib/.depend @@ -10,6 +10,10 @@ hLog.cmo: hLog.cmi hLog.cmx: hLog.cmi trie.cmo: trie.cmi trie.cmx: trie.cmi +trie.cmo: trie.cmi +trie.cmx: trie.cmi +hTopoSort.cmo: hTopoSort.cmi +hTopoSort.cmx: hTopoSort.cmi refCounter.cmo: refCounter.cmi refCounter.cmx: refCounter.cmi graphvizPp.cmo: graphvizPp.cmi diff --git a/components/extlib/Makefile b/components/extlib/Makefile index 25b49280c..f4d92191d 100644 --- a/components/extlib/Makefile +++ b/components/extlib/Makefile @@ -8,6 +8,7 @@ INTERFACE_FILES = \ patternMatcher.mli \ hLog.mli \ trie.mli \ + hTopoSort.mli \ refCounter.mli \ graphvizPp.mli \ $(NULL) diff --git a/components/extlib/graphvizPp.ml b/components/extlib/graphvizPp.ml index 4804699e0..82fa9807d 100644 --- a/components/extlib/graphvizPp.ml +++ b/components/extlib/graphvizPp.ml @@ -30,6 +30,7 @@ type attribute = string * string (* pair *) module type GraphvizFormatter = sig val header: + ?graph_type:string -> ?name:string -> ?graph_attrs:(attribute list) -> ?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) -> Format.formatter -> @@ -55,8 +56,8 @@ module Dot = attributes attrs fmt; fprintf fmt "];@]@," - let header ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt = - fprintf fmt "@[strict digraph %s {@," name; + let header ?(graph_type = "digraph") ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt = + fprintf fmt "@[%s %s {@," graph_type name; List.iter (fun (k, v) -> fprintf fmt "@[%s=@,%s;@]@," k v) graph_attrs; (match node_attrs with diff --git a/components/extlib/graphvizPp.mli b/components/extlib/graphvizPp.mli index a10831dca..79037df72 100644 --- a/components/extlib/graphvizPp.mli +++ b/components/extlib/graphvizPp.mli @@ -32,10 +32,13 @@ type attribute = string * string (* pair *) module type GraphvizFormatter = sig (** @param name graph name + * @param graph_type type of dot graph, default value "digraph" + * interesting options: "strict digraph" * @param graph_attrs graph attributes * @param node_attrs graph-wide node attributes * @param edge_attrs graph-wide edge attributes *) val header: + ?graph_type:string -> ?name:string -> ?graph_attrs:(attribute list) -> ?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) -> Format.formatter -> diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml index 3cc6c9bb5..c0364315a 100644 --- a/components/extlib/hExtlib.ml +++ b/components/extlib/hExtlib.ml @@ -180,6 +180,11 @@ let split_nth n l = | n, hd :: tl -> aux (hd :: acc) (n - 1) tl in aux [] n l +let list_last l = + let l = List.rev l in + try List.hd l with exn -> raise (Failure "HExtlib.list_last") +;; + (** {2 File predicates} *) let is_dir fname = diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli index 8de41f683..0c2206a08 100644 --- a/components/extlib/hExtlib.mli +++ b/components/extlib/hExtlib.mli @@ -78,6 +78,7 @@ val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*) val list_findopt: ('a -> 'b option) -> 'a list -> 'b option val flatten_map: ('a -> 'b list) -> 'a list -> 'b list +val list_last: 'a list -> 'a (** split_nth n l * @returns two list, the first contains at least n elements, the second the diff --git a/components/extlib/hTopoSort.ml b/components/extlib/hTopoSort.ml new file mode 100644 index 000000000..cc593d570 --- /dev/null +++ b/components/extlib/hTopoSort.ml @@ -0,0 +1,69 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module Make (OT:Map.OrderedType) = + struct + + module M = Map.Make(OT);; + + let topological_sort l find_deps = + let find_deps m x = + let deps = find_deps x in + M.add x deps m + in + (* build the partial order relation *) + let m = List.fold_left (fun m i -> find_deps m i) M.empty l in + let m = (* keep only deps inside l *) + List.fold_left + (fun m' i -> + M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') + M.empty l + in + let m = M.map (fun x -> Some x) m in + (* utils *) + let keys m = M.fold (fun i _ acc -> i::acc) m [] in + let split l m = List.filter (fun i -> M.find i m = Some []) l in + let purge l m = + M.mapi + (fun k v -> if List.mem k l then None else + match v with + | None -> None + | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) + m + in + let rec aux m res = + let keys = keys m in + let ok = split keys m in + let m = purge ok m in + let res = ok @ res in + if ok = [] then res else aux m res + in + let rc = List.rev (aux m []) in + rc + ;; + + end +;; + diff --git a/components/extlib/hTopoSort.mli b/components/extlib/hTopoSort.mli new file mode 100644 index 000000000..5cd15fbf1 --- /dev/null +++ b/components/extlib/hTopoSort.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +module Make : + functor (OT : Map.OrderedType) -> + sig + module M : Map.S with type key = OT.t + val topological_sort : + M.key list -> (M.key -> M.key list) -> M.key list + end diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index b4c18726c..b516d393e 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -118,7 +118,7 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 8 +let magic = 9 type 'obj command = | Default of loc * string * UriManager.uri list @@ -127,7 +127,7 @@ type 'obj command = | Drop of loc | Print of loc * string | Qed of loc - | Coercion of loc * UriManager.uri * bool (* add composites *) + | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *) | Obj of loc * 'obj type ('term, 'lazy_term, 'reduction, 'ident) tactical = diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index c7db02872..b78f6d90b 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -218,8 +218,8 @@ let pp_default what uris = sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites = - sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri) +let pp_coercion uri do_composites arity = + sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity (if do_composites then "compounds" else "no compounds") let pp_command ~obj_pp = function @@ -228,7 +228,7 @@ let pp_command ~obj_pp = function | Drop _ -> "drop" | Print (_,s) -> "print " ^ s | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites + | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i | Obj (_,obj) -> obj_pp obj | Default (_,what,uris) -> pp_default what uris diff --git a/components/grafite/grafiteMarshal.ml b/components/grafite/grafiteMarshal.ml index e786d5001..2b1ed9dba 100644 --- a/components/grafite/grafiteMarshal.ml +++ b/components/grafite/grafiteMarshal.ml @@ -44,8 +44,8 @@ let rehash_cmd_uris = | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) - | GrafiteAst.Coercion (loc, uri, close) -> - GrafiteAst.Coercion (loc, rehash_uri uri, close) + | GrafiteAst.Coercion (loc, uri, close, arity) -> + GrafiteAst.Coercion (loc, rehash_uri uri, close, arity) | cmd -> prerr_endline "Found a command not expected in a .moo:"; let obj_pp _ = assert false in diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 9e524b377..2de83bc40 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -414,8 +414,8 @@ type 'a eval_executable = type 'a eval_from_moo = { efm_go: GT.status -> string -> GT.status } -let coercion_moo_statement_of uri = - GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false) +let coercion_moo_statement_of arity uri = + GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity) let refinement_toolkit = { RefinementTool.type_of_aux' = @@ -440,11 +440,12 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri = +let eval_coercion status ~add_composites uri arity = let status,compounds = - GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in + GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity + in let moo_content = - List.map coercion_moo_statement_of (uri::compounds) + List.map (coercion_moo_statement_of arity) (uri::compounds) in let status = GT.add_moo_content moo_content status in {status with GT.proof_status = GT.No_proof}, @@ -551,7 +552,11 @@ let add_coercions_of_record_to_moo obj lemmas status = let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in let attrs = CicUtil.attributes_of_obj obj in - List.mem (`Class `Coercion) attrs + try + match List.find + (function `Class (`Coercion _) -> true | _-> false) attrs + with `Class (`Coercion n) -> true,n | _ -> assert false + with Not_found -> false,0 with Not_found -> assert false in (* looking at the fields we can know the 'wanted' coercions, but not the @@ -561,9 +566,9 @@ let add_coercions_of_record_to_moo obj lemmas status = let wanted_coercions = HExtlib.filter_map (function - | (name,true) -> + | (name,true,arity) -> Some - (UriManager.uri_of_string + (arity, UriManager.uri_of_string (GT.qualify status name ^ ".con")) | _ -> None) fields @@ -576,13 +581,22 @@ let add_coercions_of_record_to_moo obj lemmas status = List.split (HExtlib.filter_map (fun uri -> - let is_a_wanted_coercion = - List.exists (UriManager.eq uri) wanted_coercions + let is_a_wanted_coercion,arity_wanted = + try + let arity,_ = + List.find (fun (n,u) -> UriManager.eq u uri) + wanted_coercions + in + true, arity + with Not_found -> false, 0 in - if is_a_coercion uri || is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of uri) + let is_a_coercion, arity_coercion = is_a_coercion uri in + if is_a_coercion then + Some (uri, coercion_moo_statement_of arity_coercion uri) + else if is_a_wanted_coercion then + Some (uri, coercion_moo_statement_of arity_wanted uri) else - None) + None) lemmas) in (*prerr_endline "actual coercions:"; @@ -681,8 +695,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status, lemmas = add_obj uri obj status in {status with GT.proof_status = GT.No_proof}, uri::lemmas - | GrafiteAst.Coercion (loc, uri, add_composites) -> - eval_coercion status ~add_composites uri + | GrafiteAst.Coercion (loc, uri, add_composites, arity) -> + eval_coercion status ~add_composites uri arity | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index 4809bd2e5..7b4bdfb5e 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -32,8 +32,9 @@ let add_obj refinement_toolkit uri obj status = {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects}, lemmas -let add_coercion refinement_toolkit ~add_composites status uri = - let compounds = LibrarySync.add_coercion ~add_composites refinement_toolkit uri in +let add_coercion refinement_toolkit ~add_composites status uri arity = + let compounds = + LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions}, compounds diff --git a/components/grafite_engine/grafiteSync.mli b/components/grafite_engine/grafiteSync.mli index 5e384a47a..8453dd645 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -31,7 +31,7 @@ val add_obj: val add_coercion: RefinementTool.kit -> add_composites:bool -> GrafiteTypes.status -> - UriManager.uri -> + UriManager.uri -> int -> GrafiteTypes.status * UriManager.uri list val time_travel: diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index c4e12ac08..9373e54b4 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -386,8 +386,14 @@ EXTEND SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; fields = LIST0 [ name = IDENT ; - coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; - ty = term -> (name,ty,coercion) + coercion = [ + SYMBOL ":" -> false,0 + | SYMBOL ":"; SYMBOL ">" -> true,0 + | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity + ]; + ty = term -> + let b,n = coercion in + (name,ty,b,n) ] SEP SYMBOL ";"; SYMBOL "}" -> let params = List.fold_right @@ -561,8 +567,9 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI -> - GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true) + | IDENT "coercion" ; suri = URI ; arity = OPT int -> + let arity = match arity with None -> 0 | Some x -> x in + GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> diff --git a/components/lexicon/lexiconAst.ml b/components/lexicon/lexiconAst.ml index 9fb188d48..65bb7ce64 100644 --- a/components/lexicon/lexiconAst.ml +++ b/components/lexicon/lexiconAst.ml @@ -36,7 +36,7 @@ type alias_spec = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 5 +let magic = 6 type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *) diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 9a9ddb62b..33309f109 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -43,12 +43,12 @@ let get_closure_coercions src tgt uri coercions = | CoercDb.Uri _, CoercDb.Uri _ -> let c_from_tgt = List.filter - (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) + (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) coercions in let c_to_src = List.filter - (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt)) + (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) coercions in (HExtlib.flatten_map @@ -70,31 +70,37 @@ let get_closure_coercions src tgt uri coercions = | _ -> [] (* do not close in case source or target is not an indty ?? *) ;; -let obj_attrs = [`Class `Coercion; `Generated] +let obj_attrs n = [`Class (`Coercion n); `Generated] exception UnableToCompose (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure rt c1 c2 univ = +let generate_composite_closure rt c1 c2 univ arity = let module RT = RefinementTool in let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in - let rec mk_implicits n = - match n with - | 0 -> [] - | _ -> (Cic.Implicit None) :: mk_implicits (n-1) + let rec mk_implicits = function + | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) in - let rec mk_lambda_spline c = function + let rec mk_lambda_spline c namer = function | 0 -> c | n -> Cic.Lambda - (Cic.Name ("A" ^ string_of_int (n-1)), + (namer n, (Cic.Implicit None), - mk_lambda_spline c (n-1)) + mk_lambda_spline c namer (n-1)) in - let rec count_saturations_needed n = function - | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t - | _ -> n + let count_saturations_needed t arity = + let rec aux acc n = function + | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> + aux (acc@[name]) (n+1) t + | _ -> n,acc + in + let len,names = aux [] 0 t in + let len = len - arity in + List.fold_left + (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[]) + names in let compose c1 nc1 c2 nc2 = Cic.Lambda @@ -103,11 +109,21 @@ let generate_composite_closure rt c1 c2 univ = Cic.Appl ( c2 :: mk_implicits nc2 @ [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ])) in +(* let order_metasenv metasenv = - List.sort - (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2) - metasenv + let module OT = struct type t = int let compare = Pervasives.compare end in + let module S = HTopoSort.Make (OT) in + let dep i = + let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in + let metas = List.map fst (CicUtil.metas_of_term ty) in + HExtlib.list_uniq (List.sort Pervasives.compare metas) + in + let om = + S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep + in + List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om in +*) let rec create_subst_from_metas_to_rels n = function | [] -> [] | (metano, ctx, ty)::tl -> @@ -128,26 +144,77 @@ let generate_composite_closure rt c1 c2 univ = in aux t in + let order_body_menv term body_metasenv = + let rec purge_lambdas = function + | Cic.Lambda (_,_,t) -> purge_lambdas t + | t -> t + in + let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in + let metas_that_saturate l = + List.fold_left + (fun (acc,n) t -> + let metas = CicUtil.metas_of_term t in + let metas = List.map fst metas in + let metas = + List.filter + (fun i -> List.for_all (fun (j,_) -> j<>i) acc) + metas + in + let metas = List.map (fun i -> i,n) metas in + metas @ acc, n+1) + ([],0) l + in + let l_c2 = skip_appl (purge_lambdas term) in + let l_c1 = + match HExtlib.list_last l_c2 with + | Cic.Appl l -> List.tl l + | _ -> assert false + in + (* i should cut off the laet elem of l_c2 *) + let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in + List.sort + (fun (i,ctx1,ty1) (j,ctx1,ty1) -> + try List.assoc i meta2no - List.assoc j meta2no + with Not_found -> assert false) + body_metasenv + in + let namer l n = + let l = List.map (function Cic.Name s -> s | _ -> "A") l in + let l = List.fold_left + (fun acc s -> + let rec add' s = + if List.exists ((=) s) acc then add' (s^"'") else s + in + acc@[add' s]) + [] l + in + let l = List.rev l in + Cic.Name (List.nth l (n-1)) + in debug_print (lazy ("\nCOMPOSING")); debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty)); debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty)); - let saturations_for_c1 = count_saturations_needed 0 c1_ty in - let saturations_for_c2 = count_saturations_needed 0 c2_ty in + let saturations_for_c1, names_c1 = count_saturations_needed c1_ty arity in + let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 in let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in let spline_len = saturations_for_c1 + saturations_for_c2 in - let c = mk_lambda_spline c spline_len in - (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *) + let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in + debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); let c, univ = match rt.RT.type_of_aux' [] [] c univ with | RT.Success (term, ty, metasenv, ugraph) -> debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); - let metasenv = order_metasenv metasenv in - debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); +(* let metasenv = order_metasenv metasenv in *) +(* debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); *) let body_metasenv, lambdas_metasenv = split_metasenv metasenv spline_len in +(* debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv)); +*) + let body_metasenv = order_body_menv term body_metasenv in + debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); let subst = create_subst_from_metas_to_rels spline_len body_metasenv in debug_print (lazy("SUBST: "^rt.RT.ppsubst subst)); let term = rt.RT.apply_subst subst term in @@ -174,7 +241,7 @@ let generate_composite_closure rt c1 c2 univ = let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in obj,univ ;; @@ -201,26 +268,33 @@ let mangle s t l = exception ManglingFailed of string -let number_if_already_defined buri name = +let number_if_already_defined buri name l = + let err () = + raise + (ManglingFailed + ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con")) + in let rec aux n = let suffix = if n > 0 then string_of_int n else "" in - let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in - try - let _ = Http_getter.resolve ~writable:true uri in - if Http_getter.exists uri then + let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in + let uri = UriManager.uri_of_string suri in + let retry () = + if n < 100 then begin - HLog.warn ("Uri " ^ uri ^ " already exists."); - if n < 10 then aux (n+1) else - raise - (ManglingFailed - ("Unable to give an altenative name to " ^ - buri ^ "/" ^ name ^ ".con")) + HLog.warn ("Uri " ^ suri ^ " already exists."); + aux (n+1) end else - UriManager.uri_of_string uri - with - | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri - | Http_getter_types.Unresolvable_URI _ -> assert false + err () + in + if List.exists (UriManager.eq uri) l then retry () + else + try + let _ = Http_getter.resolve' ~writable:true uri in + if Http_getter.exists' uri then retry () else uri + with + | Http_getter_types.Key_not_found _ -> uri + | Http_getter_types.Unresolvable_URI _ -> assert false in aux 0 ;; @@ -235,23 +309,24 @@ let close_coercion_graph rt src tgt uri = let todo_list = filter_duplicates todo_list coercions in try let new_coercions = - HExtlib.filter_map ( - fun (src, l , tgt) -> + List.fold_left ( + fun acc (src, l , tgt) -> try (match l with | [] -> assert false | he :: tl -> + let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in let first_step = Cic.Constant ("", Some (CoercDb.term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs) + Cic.Sort Cic.Prop, [], obj_attrs arity) in let o,_ = List.fold_left (fun (o,univ) coer -> match o with | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure rt c - (CoercDb.term_of_carr (CoercDb.Uri coer)) univ + generate_composite_closure rt c + (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity | _ -> assert false ) (first_step, CicUniv.empty_ugraph) tl in @@ -260,16 +335,19 @@ let close_coercion_graph rt src tgt uri = let by = List.map UriManager.name_of_uri l in let name = mangle name_tgt name_src by in let buri = UriManager.buri_of_uri uri in - let c_uri = number_if_already_defined buri name in + let c_uri = + number_if_already_defined buri name + (List.map (fun (_,_,u,_) -> u) acc) + in let named_obj = match o with | Cic.Constant (_,bo,ty,vl,attrs) -> Cic.Constant (name,bo,ty,vl,attrs) | _ -> assert false in - Some ((src,tgt,c_uri,named_obj))) - with UnableToCompose -> None - ) todo_list + (src,tgt,c_uri,named_obj))::acc + with UnableToCompose -> acc + ) [] todo_list in new_coercions with ManglingFailed s -> HLog.error s; [] diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index 3a4dac726..9a1fdb0ea 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -25,7 +25,13 @@ (* $Id$ *) -type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term +type coerc_carr = + | Uri of UriManager.uri + | Sort of Cic.sort + | Term of Cic.term + | Fun of int +;; + exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed @@ -56,6 +62,8 @@ let rec name_of_carr = function | Term t -> prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); "FixTheNameMangler" + | Fun i -> "FunClass_" ^ string_of_int i +;; let eq_carr src tgt = match src, tgt with @@ -71,35 +79,54 @@ let eq_carr src tgt = (lazy ("Unsupported carr for coercions: " ^ CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) else raise EqCarrOnNonMetaClosed + | Fun _,Fun _ -> true (* only one Funclass? *) +(* | Fun i,Fun j when i=j -> true *) | _, _ -> false +;; let to_list () = - !db + List.map (fun (s,t,l) -> s,t,List.map fst l) !db +;; let rec myfilter p = function | [] -> [] | (s,t,l)::tl -> - let l = List.filter (fun u -> not (p (s,t,u))) l in + let l = + HExtlib.filter_map + (fun (u,n) -> + if p (s,t,u) then + if n = 1 then + None + else + Some (u,n-1) + else + Some (u,n)) + l + in if l = [] then myfilter p tl else (s,t,l)::myfilter p tl ;; let remove_coercion p = db := myfilter p !db;; let find_coercion f = - List.flatten - (List.map - (fun (_,_,x) -> x) - (List.filter (fun (s,t,_) -> f (s,t)) !db)) + List.map + fst + (List.flatten + (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) ;; let is_a_coercion u = - List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db + List.exists + (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) + !db ;; let get_carr uri = try let src, tgt, _ = - List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db + List.find + (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl) + !db in src, tgt with Not_found -> assert false (* uri must be a coercion *) @@ -108,6 +135,7 @@ let get_carr uri = let term_of_carr = function | Uri u -> CicUtil.term_of_uri u | Sort s -> Cic.Sort s + | Fun _ -> assert false | Term _ -> assert false ;; @@ -116,10 +144,18 @@ let add_coercion (src,tgt,u) = let where = List.filter (fun (s,t,_) -> f s t) !db in let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in match where with - | [] -> db := (src,tgt,[u]) :: !db + | [] -> db := (src,tgt,[u,1]) :: !db | (src,tgt,l)::tl -> assert (tl = []); (* not sure, this may be a feature *) - db := (src,tgt,u::l)::tl @ rest + if List.exists (fun (x,_) -> UriManager.eq u x) l then + let l' = List.map + (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n)) + l + in + db := (src,tgt,l')::tl @ rest + else + db := (src,tgt,(u,1)::l)::tl @ rest + ;; diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index 92d4b7f24..d8a8b0574 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -36,6 +36,8 @@ type coerc_carr = | Uri of UriManager.uri (* const, mutind, mutconstr *) | Sort of Cic.sort (* Prop, Set, Type *) | Term of Cic.term (* nothing supported *) + | Fun of int +;; exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index 40d628125..99ba33c33 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -37,7 +37,7 @@ let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* searches a coercion fron src to tgt in the !coercions list *) -let look_for_coercion src tgt = +let look_for_coercion' src tgt = let arity_of con = try let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in @@ -77,8 +77,16 @@ let look_for_coercion src tgt = None -> NoCoercion | Some ul -> let cl = List.map CicUtil.term_of_uri ul in + let funclass_arityl = + let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in + List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl + in let arityl = List.map arity_of cl in - let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in + let argsl = + List.map2 + (fun arity fn_arity -> + mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl + in let newtl = List.map2 (fun args c -> @@ -96,7 +104,7 @@ let look_for_coercion src tgt = let look_for_coercion src tgt = let src_uri = CoercDb.coerc_carr_of_term src in let tgt_uri = CoercDb.coerc_carr_of_term tgt in - look_for_coercion src_uri tgt_uri + look_for_coercion' src_uri tgt_uri let is_a_coercion t = try @@ -109,13 +117,15 @@ let source_of t = let uri = CicUtil.uri_of_term t in CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) - -let target_of t = + +let is_a_coercion_to_funclass t = try let uri = CicUtil.uri_of_term t in - CoercDb.term_of_carr (snd (CoercDb.get_carr uri)) - with Invalid_argument _ -> assert false (* t must be a coercion *) - + match snd (CoercDb.get_carr uri) with + | CoercDb.Fun i -> Some i + | _ -> None + with Invalid_argument _ -> None + let generate_dot_file () = let module Pp = GraphvizPp.Dot in let buf = Buffer.create 10240 in @@ -145,5 +155,20 @@ let generate_dot_file () = l; Pp.trailer fmt; Buffer.contents buf +;; + +let is_composite t = + try + let uri = + match t with + | Cic.Appl (he::_) -> CicUtil.uri_of_term he + | _ -> CicUtil.uri_of_term t + in + match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + | Cic.Constant (_,_, _, _, attrs),_ -> + List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs + | _ -> false + with Invalid_argument _ -> false +;; (* EOF *) diff --git a/components/library/coercGraph.mli b/components/library/coercGraph.mli index 01f3fecf6..9e99d68f8 100644 --- a/components/library/coercGraph.mli +++ b/components/library/coercGraph.mli @@ -36,9 +36,18 @@ type coercion_search_result = val look_for_coercion : Cic.term -> Cic.term -> coercion_search_result +val look_for_coercion' : + CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result + val is_a_coercion: Cic.term -> bool +val is_a_coercion_to_funclass: Cic.term -> int option + +(* checks if term is a constant or + * a constant applyed that is marked with (`Class `Coercion) *) +val is_composite: Cic.term -> bool + + val source_of: Cic.term -> Cic.term -val target_of: Cic.term -> Cic.term val generate_dot_file: unit -> string diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 1db8f0cfc..9529375ae 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -209,7 +209,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~add_composites refinement_toolkit uri = +let add_coercion ~add_composites refinement_toolkit uri arity = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -225,23 +225,44 @@ let add_coercion ~add_composites refinement_toolkit uri = * should we saturate it with metas in case we insert it? * *) - let extract_last_two_p ty = + let spline2list ty = let rec aux = function - | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> - aux t - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false + | Cic.Prod( _, src, tgt) -> src::aux tgt + | t -> [t] in aux ty in + let src_carr, tgt_carr = + let list_remove_from_tail n l = + let rec aux n = function + | hd::tl when n > 0 -> aux (n-1) tl + | l when n = 0 -> l + | _ -> assert false + in + aux n (List.rev l) + in + let types = spline2list coer_ty in + match arity, list_remove_from_tail arity types with + | 0,tgt::src::_ -> + (* if ~delta is true, it is impossible to define an identity coercion *) + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) + | n,_::src::_ -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), + CoercDb.Fun arity + | _ -> assert false + in let already_in = List.exists - (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul) + (fun (s,t,ul) -> + List.exists + (fun u -> + UriManager.eq u uri && + CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr) + ul) (CoercDb.to_list ()) in - let ty_src, ty_tgt = extract_last_two_p coer_ty in - let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in - let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in if not add_composites then (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) else @@ -317,10 +338,13 @@ let remove_coercion uri = let generate_projections refinement_toolkit uri fields = let uris = ref [] in - let projections = CicRecord.projections_of uri (List.map fst fields) in + let projections = + CicRecord.projections_of uri + (List.map (fun (x,_,_) -> x) fields) + in try List.iter2 - (fun (uri, name, bo) (_name, coercion) -> + (fun (uri, name, bo) (_name, coercion, arity) -> try let ty, ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in @@ -331,7 +355,8 @@ let generate_projections refinement_toolkit uri fields = if coercion then begin (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) - let x = add_coercion ~add_composites:true refinement_toolkit uri + let x = + add_coercion ~add_composites:true refinement_toolkit uri arity in (*prerr_endline ("are: "); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index 61e2b2515..06b1010ab 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -47,7 +47,7 @@ val remove_obj: UriManager.uri -> unit (* The list of added objects is returned. *) val add_coercion: add_composites:bool -> - RefinementTool.kit -> UriManager.uri -> + RefinementTool.kit -> UriManager.uri -> int (* arity *) -> UriManager.uri list (* inverse of add_coercion, removes both the eventually created composite *) diff --git a/components/metadata/metadataConstraints.ml b/components/metadata/metadataConstraints.ml index 6cab493fc..cb8460147 100644 --- a/components/metadata/metadataConstraints.ml +++ b/components/metadata/metadataConstraints.ml @@ -174,17 +174,21 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) = let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables (metadata: MetadataTypes.constr list) = - let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables - in + let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in if (metadata = []) && concl_card = None && full_card = None then - failwith "MetadataQuery.at_least: no constraints given"; - let (n,from,where) = - List.fold_left (add_constraint ~tables) (0,[],[]) metadata - in - let (n,from,where) = - add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff - in - exec ~dbd ?rating (n,from,where) + begin + HLog.warn "MetadataConstraints.at_least: no constraints given"; + [] + end + else + let (n,from,where) = + List.fold_left (add_constraint ~tables) (0,[],[]) metadata + in + let (n,from,where) = + add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff + in + exec ~dbd ?rating (n,from,where) +;; let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating diff --git a/components/metadata/metadataDeps.ml b/components/metadata/metadataDeps.ml index 91fa8004c..b393dbb91 100644 --- a/components/metadata/metadataDeps.ml +++ b/components/metadata/metadataDeps.ml @@ -132,7 +132,7 @@ struct (*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*) assert false in - Pp.header ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt; + Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt; let rec aux = function | [] -> () diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 9baf829ea..192460633 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -419,8 +419,17 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: = let module C = Cic in let curi,metasenv,pbo,pty = proof in + (* occur check *) + let occur i t = + let m = CicUtil.metas_of_term t in + List.exists (fun (j,_) -> i=j) m + in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let _,_ = (* TASSI: FIXME *) + if occur metano term then + raise + (ProofEngineTypes.Fail (lazy + "You can't letin a term containing the current goal")); + let _,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in let newmeta = new_meta_of_proof ~proof in let fresh_name = diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 4517db0b5..862f78161 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Aug 31 14:46:00 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic diff --git a/matita/lablGraphviz.ml b/matita/lablGraphviz.ml index 12d302d24..27e7d4b9a 100644 --- a/matita/lablGraphviz.ml +++ b/matita/lablGraphviz.ml @@ -31,13 +31,12 @@ type attribute = string * string (* pair *) let png_flags = "-Tpng" let map_flags = "-Tcmapx" -let tred_cmd = "tred" (* graphviz transitive reduction filter *) let tempfile () = Filename.temp_file "matita_" "" class type graphviz_widget = object - method load_graph_from_file: string -> unit + method load_graph_from_file: ?gviz_cmd:string -> string -> unit method connect_href: (GdkEvent.Button.t -> (string * string) list -> unit) -> unit method center_on_href: string -> unit @@ -45,10 +44,10 @@ class type graphviz_widget = method as_viewport: GBin.viewport end -class graphviz_impl ?packing gviz_cmd = +class graphviz_impl ?packing () = let viewport = GBin.viewport ?packing () in - let mk_gviz_cmd flags src_fname dest_fname = - sprintf "cat %s | %s | %s %s > %s" src_fname tred_cmd gviz_cmd flags + let mk_gviz_cmd gviz_cmd flags src_fname dest_fname = + sprintf "cat %s | %s %s > %s" src_fname gviz_cmd flags dest_fname in let image = GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 () @@ -70,9 +69,9 @@ class graphviz_impl ?packing gviz_cmd = (try href_cb button (self#find_href x y) with Not_found -> ()); false)) - method load_graph_from_file fname = + method load_graph_from_file ?(gviz_cmd = "dot") fname = let tmp_png = tempfile () in - let rc = Sys.command (mk_gviz_cmd png_flags fname tmp_png) in + let rc = Sys.command (mk_gviz_cmd gviz_cmd png_flags fname tmp_png) in if rc <> 0 then eprintf ("Graphviz command failed (exit code: %d) on the following graph:\n" @@ -81,7 +80,7 @@ class graphviz_impl ?packing gviz_cmd = image#set_file tmp_png; HExtlib.safe_remove tmp_png; let tmp_map = tempfile () in - ignore (Sys.command (mk_gviz_cmd map_flags fname tmp_map)); + ignore (Sys.command (mk_gviz_cmd gviz_cmd map_flags fname tmp_map)); self#load_map tmp_map; HExtlib.safe_remove tmp_map @@ -128,12 +127,6 @@ class graphviz_impl ?packing gviz_cmd = end -let factory cmd ?packing () = - (new graphviz_impl ?packing cmd :> graphviz_widget) - -let gDot = factory "dot" -let gNeato = factory "neato" -let gTwopi = factory "twopi" -let gCirco = factory "circo" -let gFdp = factory "fdp" +let graphviz ?packing () = + (new graphviz_impl ?packing () :> graphviz_widget) diff --git a/matita/lablGraphviz.mli b/matita/lablGraphviz.mli index d6b7f4f6e..7b90eec12 100644 --- a/matita/lablGraphviz.mli +++ b/matita/lablGraphviz.mli @@ -38,8 +38,13 @@ class type graphviz_widget = * GtkImage widget * 2) render it to a (HTML) map, internalizing its data. * Remember that map entries are generated only for nodes, (edges, ...) - * that have an "href" (or "URL", a synonym) attribute *) - method load_graph_from_file: string -> unit + * that have an "href" (or "URL", a synonym) attribute + * Interesting values for gviz_cmd are: + * 'neato' + * 'dot' + * 'tred | dot' + *) + method load_graph_from_file: ?gviz_cmd:string -> string -> unit (** Callback invoked when a click on a node listed in the map is received. * @param gdk's button event @@ -63,9 +68,5 @@ class type graphviz_widget = (** {2 Constructors} *) -val gDot: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget -val gNeato: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget -val gTwopi: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget -val gCirco: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget -val gFdp: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget +val graphviz: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget diff --git a/matita/library/legacy/coq.ma b/matita/library/legacy/coq.ma index 31a5f35ee..9860c63e2 100644 --- a/matita/library/legacy/coq.ma +++ b/matita/library/legacy/coq.ma @@ -19,9 +19,9 @@ default "equality" cic:/Coq/Init/Logic/sym_eq.con cic:/Coq/Init/Logic/trans_eq.con cic:/Coq/Init/Logic/eq_ind.con - cic:/Coq/Init/Logic/eq_ind_r.con - cic:/Coq/Init/Logic/f_equal.con - cic:/Coq/Init/Logic/f_equal1.con. + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/f_equal.con + cic:/matita/legacy/coq/f_equal1.con. default "true" cic:/Coq/Init/Logic/True.ind. @@ -75,17 +75,16 @@ interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/n interpretation "Coq's natural 'not less or equal than'" 'nleq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)). - + +theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A. + x = y \to (f y) = (f x). + intros. + symmetry. + apply cic:/Coq/Init/Logic/f_equal.con. + assumption. +qed. (* aliases *) (* FG: This is because "and" is a reserved keyword of the parser *) alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)". -(* theorems *) - -theorem f_equal1 : - \forall A,B:Type. \forall f:A \to B. \forall x,y:A. - x = y \to f y = f x. - intros.elim H.reflexivity. -qed. - diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma index 129b00189..c26449c42 100644 --- a/matita/library/logic/equality.ma +++ b/matita/library/logic/equality.ma @@ -60,6 +60,14 @@ theorem eq_elim_r: intros. elim (sym_eq ? ? ? H1).assumption. qed. +theorem eq_f: \forall A,B:Type.\forall f:A\to B. +\forall x,y:A. x=y \to f x = f y. +intros.elim H.reflexivity. +qed. + +coercion cic:/matita/logic/equality/sym_eq.con. +coercion cic:/matita/logic/equality/eq_f.con. + default "equality" cic:/matita/logic/equality/eq.ind cic:/matita/logic/equality/sym_eq.con @@ -67,19 +75,8 @@ default "equality" cic:/matita/logic/equality/eq_ind.con cic:/matita/logic/equality/eq_elim_r.con cic:/matita/logic/equality/eq_f.con - cic:/matita/logic/equality/eq_f1.con. (* \x.sym (eq_f x) *) - + cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *) -theorem eq_f: \forall A,B:Type.\forall f:A\to B. -\forall x,y:A. x=y \to f x = f y. -intros.elim H.reflexivity. -qed. - -theorem eq_f1: \forall A,B:Type.\forall f:A\to B. -\forall x,y:A. x=y \to f y = f x. -intros.elim H.reflexivity. -qed. - theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C. \forall x1,x2:A. \forall y1,y2:B. x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2. diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml index c235a9f43..6976d57e0 100644 --- a/matita/matitaMathView.ml +++ b/matita/matitaMathView.ml @@ -797,7 +797,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in let gui = get_gui () in let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in - let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in + let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in let combo,_ = GEdit.combo_box_text ~strings:queries () in let activate_combo_query input q = @@ -1053,7 +1053,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let fmt = Format.formatter_of_out_channel oc in MetadataDeps.DepGraph.render fmt gviz_graph; close_out oc; - gviz#load_graph_from_file tmpfile; + gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; (match center_on with | None -> () | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri)); diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma index 914126de2..e792bd780 100644 --- a/matita/tests/coercions.ma +++ b/matita/tests/coercions.ma @@ -13,16 +13,14 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/coercions/". -include "nat/nat.ma". + +include "nat/compare.ma". +include "datatypes/bool.ma". inductive pos: Set \def | one : pos | next : pos \to pos. -inductive nat:Set \def -| O : nat -| S : nat \to nat. - inductive int: Set \def | positive: nat \to int | negative : nat \to int. @@ -60,11 +58,6 @@ definition double2: \forall f:int \to int. pos \to int \def \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)). - -coercion cic:/matita/logic/equality/eq_f.con. -coercion cic:/matita/logic/equality/eq_f1.con. -variant xxx : ? \def eq_f. -coercion cic:/matita/tests/coercions/xxx.con. theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x. intros. @@ -73,8 +66,6 @@ qed. variant pos2nat' : ? \def pos2nat. -coercion cic:/matita/tests/coercions/xxx.con. - inductive initial: Set \def iii : initial. definition i2pos: ? \def \lambda x:initial.one. @@ -83,4 +74,39 @@ coercion cic:/matita/tests/coercions/i2pos.con. coercion cic:/matita/tests/coercions/pos2nat'.con. +inductive listn (A:Type) : nat \to Type \def + | Nil : listn A O + | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n). + +definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def + \lambda A,b,a,c. + match b with + [ true \Rightarrow a + | false \Rightarrow c]. + +let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def + match l with + [ Nil \Rightarrow dummy + | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)]. + +definition listn2function: + \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A +\def + \lambda A,dummy,n,l,m.ith A n m dummy l. + +definition natlist2map: ? \def listn2function nat O. + +coercion cic:/matita/tests/coercions/natlist2map.con 1. +definition map: \forall n:nat.\forall l:listn nat n. nat \to nat \def + \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m. + +definition church: nat \to nat \to nat \def times. + +coercion cic:/matita/tests/coercions/church.con 1. + +definition mapmult: \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def + \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o. + + + \ No newline at end of file -- 2.39.2