From: Ferruccio Guidi Date: Wed, 23 Nov 2016 19:51:27 +0000 (+0000) Subject: 1) hard coded linearized references removed X-Git-Tag: make_still_working~529 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b2a542079e4c3b8b122d74d48fe2fdf234f3684c;p=helm.git 1) hard coded linearized references removed 2) new concrete syntax for linearized references more compliant with URI generic syntax and ELPI '#' not allowed in path and name Decl cic:/path/name#dec Def cic:/path/name#def:i Fix of int * int cic:/path/name#fix:i:j:h CoFix of int cic:/path/name#cfx:i Ind of int cic:/path/name#ind:b:i:l Con of int * int cic:/path/name#con:i:j:l run matitaclean all after this update, as stored aliases depend on linearized references --- diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 5c0d0a7d5..59fe713e5 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -167,7 +167,8 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) "branch pattern must be \"_\""))) ) branches in let indtype_ref = - NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)" + let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in + NRef.reference_of_spec uri (NRef.Ind (true,1,1)) in NCic.Match (indtype_ref, cic_outtype, cic_term, (List.map do_branch branches)) @@ -177,7 +178,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | Some (indty_ident, _) -> (match Disambiguate.resolve ~env ~mk_choice (DT.Id indty_ident) (`Args []) with - | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r + | NCic.Const (NRef.Ref (_,NRef.Ind _) as r) -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) @@ -205,9 +206,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) *) (match Disambiguate.resolve ~env ~mk_choice (DT.Id (fst_constructor branches)) (`Args []) with - | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> + | NCic.Const (NRef.Ref (_,NRef.Con _) as r) -> let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in - NReference.mk_indty b r + NRef.mk_indty b r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) @@ -322,7 +323,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) | NotationPt.Uri (uri, subst) -> assert (subst = None); (try - NCic.Const (NReference.reference_of_string uri) + NCic.Const (NRef.reference_of_string uri) with NRef.IllFormedReference _ -> NotationPt.fail loc "Ill formed reference") | NotationPt.NRef nref -> NCic.Const nref @@ -466,7 +467,7 @@ let interpretate_obj status List.fold_left (fun (i,res) (name,_,_,_) -> let nref = - NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno)) + NRef.reference_of_spec uri (NRef.Ind (inductive,i,leftno)) in i+1,(name,nref)::res) (0,[]) tyl) in @@ -521,7 +522,7 @@ let interpretate_obj status (interpretate_term status ~obj_context:[] ~context ~env ~uri:None ~is_path:false ty) in let nref = - NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in + NRef.reference_of_spec uri (NRef.Ind (true,0,leftno)) in let obj_context = [name,nref] in let fields' = snd ( @@ -555,9 +556,9 @@ let interpretate_obj status List.fold_left (fun (i,acc) (_,(name,_),_,k) -> (i+1, - (ncic_name_of_ident name, NReference.reference_of_spec uri - (if inductive then NReference.Fix (i,k,0) - else NReference.CoFix i)) :: acc)) + (ncic_name_of_ident name, NRef.reference_of_spec uri + (if inductive then NRef.Fix (i,k,0) + else NRef.CoFix i)) :: acc)) (0,[]) defs in let inductiveFuns = diff --git a/matita/components/ng_extraction/nCicExtraction.ml b/matita/components/ng_extraction/nCicExtraction.ml index 4e167004d..12261145e 100644 --- a/matita/components/ng_extraction/nCicExtraction.ml +++ b/matita/components/ng_extraction/nCicExtraction.ml @@ -25,11 +25,13 @@ (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *) +module Ref = NReference + let fix_sorts t = t;; let apply_subst subst t = assert (subst=[]); t;; -type typformerreference = NReference.reference -type reference = NReference.reference +type typformerreference = Ref.reference +type reference = Ref.reference type kind = | Type @@ -130,13 +132,13 @@ let rec size_of_term = | UnsafeCoerce t -> 1 + size_of_term t ;; -module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) +module ReferenceMap = Map.Make(struct type t = Ref.reference let compare = Ref.compare end) module GlobalNames = Set.Make(String) type info_el = string * [`Type of typ_context * typ option | `Constructor of typ | `Function of typ ] -type info = (NReference.reference * info_el) list +type info = (Ref.reference * info_el) list type db = info_el ReferenceMap.t * GlobalNames.t let empty_info = [] @@ -146,15 +148,16 @@ type obj_kind = | TypeDefinition of typ_former_def | TermDeclaration of term_former_decl | TermDefinition of term_former_def - | LetRec of (info * NReference.reference * obj_kind) list + | LetRec of (info * Ref.reference * obj_kind) list (* reference, left, right, constructors *) - | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list + | Algebraic of (info * Ref.reference * typ_context * typ_context * (Ref.reference * typ) list) list -type obj = info * NReference.reference * obj_kind +type obj = info * Ref.reference * obj_kind (* For LetRec and Algebraic blocks *) let dummyref = - NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" + let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in + Ref.reference_of_spec uri (Ref.Ind (true,1,1)) type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];; @@ -185,7 +188,7 @@ let rec classify_not_term status context t = classify_not_term status ((b,NCic.Decl s)::context) t | NCic.Implicit _ | NCic.LetIn _ - | NCic.Const (NReference.Ref (_,NReference.CoFix _)) + | NCic.Const (Ref.Ref (_,Ref.CoFix _)) | NCic.Appl [] -> assert false (* NOT POSSIBLE *) | NCic.Lambda (n,s,t) -> @@ -195,10 +198,10 @@ let rec classify_not_term status context t = | NCic.Match (_,_,_,pl) -> let classified_pl = List.map (classify_not_term status context) pl in sup classified_pl - | NCic.Const (NReference.Ref (_,NReference.Fix _)) -> + | NCic.Const (Ref.Ref (_,Ref.Fix _)) -> assert false (* IMPOSSIBLE *) | NCic.Meta _ -> assert false (* TODO *) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)-> + | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix (i,_,_)) as r)::_)-> let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in let _,_,_,_,bo = List.nth l i in classify_not_term status [] bo @@ -223,7 +226,7 @@ let rec classify_not_term status context t = (match List.nth context (n-1) with _,NCic.Decl typ -> find_sort typ | _,NCic.Def _ -> assert false (* IMPOSSIBLE *)) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) -> + | NCic.Const (Ref.Ref (_,Ref.Decl) as ref) -> let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in (match classify_not_term status [] ty with | `Proposition @@ -231,7 +234,7 @@ let rec classify_not_term status context t = | `Kind | `KindOrType -> `Type | `PropKind -> `Proposition) - | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) -> + | NCic.Const (Ref.Ref (_,Ref.Ind _) as ref) -> let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in let _,_,arity,_ = List.nth ityl i in (match classify_not_term status [] arity with @@ -240,8 +243,8 @@ let rec classify_not_term status context t = | `KindOrType -> assert false (* IMPOSSIBLE *) | `Kind -> `Type | `PropKind -> `Proposition) - | NCic.Const (NReference.Ref (_,NReference.Con _)) - | NCic.Const (NReference.Ref (_,NReference.Def _)) -> + | NCic.Const (Ref.Ref (_,Ref.Con _)) + | NCic.Const (Ref.Ref (_,Ref.Def _)) -> assert false (* IMPOSSIBLE *) ;; @@ -377,10 +380,10 @@ let rec split_typ_lambdas status n ~metasenv context typ = let rev_context_of_typformer status ~metasenv context = function - NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Def _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) - | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) -> + NCic.Const (Ref.Ref (_,Ref.Ind _) as ref) + | NCic.Const (Ref.Ref (_,Ref.Def _) as ref) + | NCic.Const (Ref.Ref (_,Ref.Decl) as ref) + | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref) -> (try match snd (ReferenceMap.find ref (fst status#extraction_db)) with `Type (ctx,_) -> List.rev ctx @@ -405,8 +408,8 @@ let rev_context_of_typformer status ~metasenv context = let typ = kind_of status ~metasenv typ_ctx typ in List.rev (fst (split_kind_prods [] typ)) | NCic.Meta _ -> assert false (* TODO *) - | NCic.Const (NReference.Ref (_,NReference.Con _)) - | NCic.Const (NReference.Ref (_,NReference.CoFix _)) + | NCic.Const (Ref.Ref (_,Ref.Con _)) + | NCic.Const (Ref.Ref (_,Ref.CoFix _)) | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _ | NCic.Appl _ | NCic.Prod _ -> assert false (* IMPOSSIBLE *) @@ -434,7 +437,7 @@ let rec typ_of status ~metasenv context k = | NCic.Rel n -> Var n | NCic.Const ref -> TConst ref | NCic.Match (_,_,_,_) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) -> + | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix _))::_) -> Top | NCic.Appl (he::args) -> let rev_he_context= rev_context_of_typformer status ~metasenv context he in @@ -521,7 +524,7 @@ let fomega_lookup status ref = | `Function _ -> assert false with Not_found -> -prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); None +prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); None let rec fomega_whd status ty = match ty with @@ -548,7 +551,7 @@ let rec fomega_conv status t1 t2 = Var n, Var m -> n=m | Unit, Unit -> true | Top, Top -> true - | TConst r1, TConst r2 -> NReference.eq r1 r2 + | TConst r1, TConst r2 -> Ref.eq r1 r2 | Arrow (s1,t1), Arrow (s2,t2) -> fomega_conv status s1 s2 && fomega_conv status t1 t2 | TSkip t1, TSkip t2 -> fomega_conv status t1 t2 @@ -574,11 +577,11 @@ let type_of_constructor status ref = let type_of_appl_he status ~metasenv context = function - NCic.Const (NReference.Ref (_,NReference.Con _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Def _) as ref) - | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) - | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) - | NCic.Const (NReference.Ref (_,NReference.CoFix _) as ref) -> + NCic.Const (Ref.Ref (_,Ref.Con _) as ref) + | NCic.Const (Ref.Ref (_,Ref.Def _) as ref) + | NCic.Const (Ref.Ref (_,Ref.Decl) as ref) + | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref) + | NCic.Const (Ref.Ref (_,Ref.CoFix _) as ref) -> (try match snd (ReferenceMap.find ref (fst status#extraction_db)) with `Type _ -> assert false @@ -586,7 +589,7 @@ let type_of_appl_he status ~metasenv context = | `Function ty -> ty with Not_found -> assert false) - | NCic.Const (NReference.Ref (_,NReference.Ind _)) -> + | NCic.Const (Ref.Ref (_,Ref.Ind _)) -> assert false (* IMPOSSIBLE *) | NCic.Rel n -> (match List.nth context (n-1) with @@ -685,7 +688,7 @@ let rec term_of status ~metasenv context = try HExtlib.list_mapi (fun pat i -> - let ref = NReference.mk_constructor (i+1) ref in + let ref = Ref.mk_constructor (i+1) ref in let ty = (* BUG HERE, QUICK BUG WRONG PATCH IN PLACE *) try @@ -801,7 +804,7 @@ let fresh_name_of_ref status ref = (*CSC: Patch while we wait for separate compilation *) let candidate = let name = NCicPp.r2s status true ref in - let NReference.Ref (uri,_) = ref in + let Ref.Ref (uri,_) = ref in let path = NUri.baseuri_of_uri uri in let path = String.sub path 5 (String.length path - 5) in let path = Str.global_replace (Str.regexp "/") "_" path in @@ -879,7 +882,7 @@ let object_of_inductive status ~metasenv uri ind leftno il = let ctx,_ = split_kind_prods [] arity in let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in let ref = - NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in + Ref.reference_of_spec uri (Ref.Ind (ind,i,leftno)) in let info = ref,`Type (ctx,None) in let status,info = register_name_and_info status info in let _,status,cl_rev,infos = @@ -890,7 +893,7 @@ let object_of_inductive status ~metasenv uri ind leftno il = let ty = typ_of status ~metasenv ctx ty in let left = term_ctx_of_type_ctx left in let full_ty = glue_ctx_typ left ty in - let ref = NReference.mk_constructor j ref in + let ref = Ref.mk_constructor j ref in let info = ref,`Constructor full_ty in let status,info = register_name_and_info status info in j+1,status,((ref,ty)::res),info::infos @@ -908,7 +911,7 @@ let object_of status (uri,height,metasenv,subst,obj_kind) = let obj_kind = apply_subst subst obj_kind in match obj_kind with | NCic.Constant (_,_,None,ty,_) -> - let ref = NReference.reference_of_spec uri NReference.Decl in + let ref = Ref.reference_of_spec uri Ref.Decl in (match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in @@ -927,7 +930,7 @@ let object_of status (uri,height,metasenv,subst,obj_kind) = TermDeclaration (split_typ_prods [] ty)) | `Term _ -> status, Failure "Type classified as a term. This is a bug.") | NCic.Constant (_,_,Some bo,ty,_) -> - let ref = NReference.reference_of_spec uri (NReference.Def height) in + let ref = Ref.reference_of_spec uri (Ref.Def height) in object_of_constant status ~metasenv ref bo ty | NCic.Fixpoint (fix_or_cofix,fs,_) -> let _,status,objs = @@ -935,10 +938,10 @@ let object_of status (uri,height,metasenv,subst,obj_kind) = (fun (_,_name,recno,ty,bo) (i,status,res) -> let ref = if fix_or_cofix then - NReference.reference_of_spec - uri (NReference.Fix (i,recno,height)) + Ref.reference_of_spec + uri (Ref.Fix (i,recno,height)) else - NReference.reference_of_spec uri (NReference.CoFix i) + Ref.reference_of_spec uri (Ref.CoFix i) in let status,obj = object_of_constant ~metasenv status ref bo ty in match obj with @@ -1041,7 +1044,7 @@ let classify_reference status ref = | `Function _ -> `FunctionName with Not_found -> -prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName +prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); `FunctionName ;; let capitalize classification name = @@ -1057,7 +1060,7 @@ let pp_ref status ref = capitalize (classify_reference status ref) (try fst (ReferenceMap.find ref (fst status#extraction_db)) with Not_found -> -prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref); +prerr_endline ("BUG with coercions: " ^ Ref.string_of_reference ref); (*assert false*) NCicPp.r2s status true ref (* BUG: this should never happen *) ) @@ -1146,7 +1149,7 @@ let rec pretty_print_term status ctxt = String.concat " ;\n" (HExtlib.list_mapi (fun (bound_names,rhs) i -> - let ref = NReference.mk_constructor (i+1) r in + let ref = Ref.mk_constructor (i+1) r in let name = pp_ref status ref in let ctxt,bound_names = pretty_print_term_context status ctxt bound_names in diff --git a/matita/components/ng_kernel/nReference.ml b/matita/components/ng_kernel/nReference.ml index bb560bfd6..102f25046 100644 --- a/matita/components/ng_kernel/nReference.ml +++ b/matita/components/ng_kernel/nReference.ml @@ -45,14 +45,15 @@ module MapStringsToReference = Map.Make(OrderedStrings);; let set_of_reference = ref MapStringsToReference.empty;; -(* '.' not allowed in path and foo +(* Note: valid ELPI constant + * '#' not allowed in path and name * - * Decl cic:/path/foo.dec - * Def cic:/path/foo.def - * Fix of int * int cic:/path/foo.fix(i,j) - * CoFix of int cic:/path/foo.cfx(i) - * Ind of int cic:/path/foo.ind(i) - * Con of int * int cic:/path/foo.con(i,j) + * Decl cic:/path/name#dec + * Def cic:/path/name#def:i + * Fix of int * int cic:/path/name#fix:i:j:h + * CoFix of int cic:/path/name#cfx:i + * Ind of int cic:/path/name#ind:b:i:l + * Con of int * int cic:/path/name#con:i:j:l *) let uri_suffix_of_ref_suffix = function @@ -63,11 +64,11 @@ let uri_suffix_of_ref_suffix = function let reference_of_string = let get3 s dot = - let comma2 = String.rindex s ',' in - let comma = String.rindex_from s (comma2-1) ',' in + let comma2 = String.rindex s ':' in + let comma = String.rindex_from s (comma2-1) ':' in let s_i = String.sub s (dot+5) (comma-dot-5) in let s_j = String.sub s (comma+1) (comma2-comma-1) in - let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in + let s_h = String.sub s (comma2+1) (String.length s-comma2-1) in let i = int_of_string s_i in let j = int_of_string s_j in let h = int_of_string s_h in @@ -75,14 +76,14 @@ let reference_of_string = in (* let get2 s dot = - let comma = String.rindex s ',' in + let comma = String.rindex s ':' in let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in - let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in + let j = int_of_string (String.sub s (comma+1) (String.length s-comma-1)) in i,j in *) let get1 s dot = - let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in + let i = int_of_string (String.sub s (dot+5) (String.length s-dot-5)) in i in fun s -> @@ -90,10 +91,10 @@ fun s -> with Not_found -> let new_reference = try - let dot = String.rindex s '.' in - let prefix = String.sub s 0 (dot+1) in + let dot = String.rindex s '#' in + let prefix = String.sub s 0 dot in let suffix = String.sub s (dot+1) 3 in - let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in + let u = NUri.uri_of_string (prefix ^ "." ^ uri_suffix_of_ref_suffix suffix) in match suffix with | "dec" -> Ref (u, Decl) | "def" -> let i = get1 s dot in Ref (u, Def i) @@ -113,16 +114,16 @@ let string_of_reference (Ref (u,indinfo)) = let dot = String.rindex s '.' in let s2 = String.sub s 0 dot in match indinfo with - | Decl -> s2 ^ ".dec" - | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")" + | Decl -> s2 ^ "#dec" + | Def h -> s2 ^ "#def:" ^ string_of_int h | Fix (i,j,h) -> - s2 ^ ".fix(" ^ string_of_int i ^ "," ^ - string_of_int j ^ "," ^ string_of_int h ^ ")" - | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")" - | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^ - "," ^ string_of_int l ^ ")" - | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ - "," ^ string_of_int l ^ ")" + s2 ^ "#fix:" ^ string_of_int i ^ ":" ^ + string_of_int j ^ ":" ^ string_of_int h + | CoFix i -> s2 ^ "#cfx:" ^ string_of_int i + | Ind (b,i,l)->s2 ^"#ind:" ^(if b then "1" else "0")^ ":" ^ string_of_int i ^ + ":" ^ string_of_int l + | Con (i,j,l) -> s2 ^ "#con:" ^ string_of_int i ^ ":" ^ string_of_int j ^ + ":" ^ string_of_int l ;; let mk_constructor j = function @@ -155,7 +156,3 @@ let mk_cofix i = function let reference_of_spec u spec = reference_of_string (string_of_reference (Ref (u, spec))) ;; - - - - diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index 3aabdf1d4..15fcc069a 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/components/ng_refiner/nCicRefiner.ml @@ -178,6 +178,16 @@ in name' ^ (if last = -1 then "" else string_of_int (last + 1)) with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false +(* let eq, eq_refl = + let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in + C.Const (Ref.reference_of_spec uri (Ref.Ind (true,0,2))), + C.Const (Ref.reference_of_spec uri Ref.Con (0,1,2)) +*) +let eq, eq_refl = + let uri = NUri.uri_of_string "cic:/matita/basics/jmeq/jmeq.ind" in + C.Const (Ref.reference_of_spec uri (Ref.Ind(true,0,2))), + C.Const (Ref.reference_of_spec uri (Ref.Con(0,1,2))) + let rec typeof (status:#NCicCoercion.status) ?(localise=fun _ -> Stdpp.dummy_loc) metasenv subst context term expty @@ -603,7 +613,7 @@ and try_coercions status (* {{{ helper functions *) let get_cl_and_left_p refit outty = match refit with - | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) -> + | Ref.Ref (uri, Ref.Ind (_,tyno,leftno)) -> let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in let _, _, ty, cl = List.nth itl tyno in let constructorsno = List.length cl in @@ -678,10 +688,6 @@ and try_coercions status (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1)) | _ -> assert false in - (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in - let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) - let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in - let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in let add_params metasenv subst context cty outty mty m i = @@ -1014,8 +1020,8 @@ and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s) and guess_name status subst ctx ty = let aux initial = "#" ^ String.make 1 initial in match ty with - | C.Const (NReference.Ref (u,_)) - | C.Appl (C.Const (NReference.Ref (u,_)) :: _) -> + | C.Const (Ref.Ref (u,_)) + | C.Appl (C.Const (Ref.Ref (u,_)) :: _) -> aux (String.sub (NUri.name_of_uri u) 0 1).[0] | C.Prod _ -> aux 'f' | C.Meta (n,lc) -> @@ -1106,7 +1112,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig aux metasenv subst (arg :: args_so_far) he meta tl | C.Match (_,_,C.Meta _,_) | C.Match (_,_,C.Appl (C.Meta _ :: _),_) - | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) -> + | C.Appl (C.Const (Ref.Ref (_, Ref.Fix _)) :: _) -> raise (Uncertain (lazy (localise orig_he, Printf.sprintf ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (status#ppterm ~metasenv ~subst ~context he) @@ -1171,8 +1177,8 @@ let undebruijnate status inductive ref t rev_fl = (fun (_,_,rno,_,_,_) i -> let i = len - i - 1 in C.Const - (if inductive then NReference.mk_fix i rno ref - else NReference.mk_cofix i ref)) + (if inductive then Ref.mk_fix i rno ref + else Ref.mk_cofix i ref)) rev_fl) t ;; @@ -1224,9 +1230,9 @@ let typeof_obj (fun (relevance,name,k,ty,dbo) -> let bo = undebruijnate status inductive - (NReference.reference_of_spec uri - (if inductive then NReference.Fix (0,k,0) - else NReference.CoFix 0)) dbo rev_fl + (Ref.reference_of_spec uri + (if inductive then Ref.Fix (0,k,0) + else Ref.CoFix 0)) dbo rev_fl in relevance,name,k,ty,bo) fl @@ -1365,8 +1371,8 @@ let typeof_obj if i <= leftno then C.Rel i else - C.Const (NReference.reference_of_spec uri - (NReference.Ind (ind,relsno - i,leftno)))) + C.Const (Ref.reference_of_spec uri + (Ref.Ind (ind,relsno - i,leftno)))) (HExtlib.list_seq 1 (relsno+1)) te in let te = diff --git a/matita/components/ng_refiner/nCicUnifHint.ml b/matita/components/ng_refiner/nCicUnifHint.ml index ff8de7554..a0d767c3a 100644 --- a/matita/components/ng_refiner/nCicUnifHint.ml +++ b/matita/components/ng_refiner/nCicUnifHint.ml @@ -11,6 +11,8 @@ (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) +module Ref = NReference + let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; @@ -62,7 +64,10 @@ class virtual status = = fun o -> {< db = o#uhint_db >} end -let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");; +let dummy = + let uri = NUri.uri_of_string "cic:/matita/dummy/dec.con" in + NCic.Const (Ref.reference_of_spec uri Ref.Decl);; + let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;; let index_hint status context t1 t2 precedence = @@ -176,11 +181,11 @@ let db () = in let n1 = NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri - u1 (NReference.Def h1)) :: mk_rels (List.length ctx)) + u1 (Ref.Def h1)) :: mk_rels (List.length ctx)) in let n2 = NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri - u2 (NReference.Def h2)) :: mk_rels (List.length ctx)) + u2 (Ref.Def h2)) :: mk_rels (List.length ctx)) in [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2] end else []