X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=bfe12cee70bf5174000fd9cd44ed6a539a43d1bc;hb=164332b640d2c2e601350065b0074ba80426ea5c;hp=267b40a20af91da6c3535e12bcfde75f4c24e833;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 267b40a20..bfe12cee7 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,17 +27,26 @@ let cic_name_of_name = function | _ -> assert false ;; -let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization_tbl = +let refine_term + metasenv subst context uri ~coercion_db ~use_coercions term _ ~localization_tbl= assert (uri=None); debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (NCicPp.ppterm ~metasenv ~subst ~context term))); try let localise t = try NCicUntrusted.NCicHash.find localization_tbl t - with Not_found -> assert false + with Not_found -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); + assert false in let metasenv, subst, term, _ = - NCicRefiner.typeof metasenv subst context term None ~localise + NCicRefiner.typeof + (NCicUnifHint.db ()) + ~look_for_coercion:( + if use_coercions then + NCicCoercion.look_for_coercion coercion_db + else (fun _ _ _ _ _ -> [])) + metasenv subst context term None ~localise in Disambiguate.Ok (term, metasenv, subst, ()) with @@ -62,7 +71,7 @@ let find_in_context name context = let interpretate_term ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast - ~localization_tbl + ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); @@ -70,8 +79,9 @@ let interpretate_term let rec aux ~localize loc context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in - if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; - res + if localize then + NCicUntrusted.NCicHash.add localization_tbl res loc; + res | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in @@ -128,14 +138,15 @@ let interpretate_term | Some (indty_ident, _) -> (match Disambiguate.resolve ~env ~mk_choice (Id indty_ident) (`Args []) with - | NCic.Const r -> r + | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) - | _ -> + | t -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched "^ - "is not (co)inductive!")))) + "is not (co)inductive: " ^ NCicPp.ppterm + ~metasenv:[] ~subst:[] ~context:[] t)))) | None -> let rec fst_constructor = function @@ -146,16 +157,26 @@ let interpretate_term "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) in - (match Disambiguate.resolve ~env ~mk_choice +(* + DisambiguateTypes.Environment.iter + (fun k v -> + prerr_endline + (DisambiguateTypes.string_of_domain_item k ^ " => " ^ + description_of_alias v)) env; +*) + (match Disambiguate.resolve ~env ~mk_choice (Id (fst_constructor branches)) (`Args []) with - | NCic.Const r -> r + | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> + let b,_,_,_,_ = NCicEnvironment.get_checked_indtys r in + NReference.mk_indty b r | NCic.Implicit _ -> raise (Disambiguate.Try_again (lazy "The type of the term to be matched is still unknown")) - | _ -> + | t -> raise (DisambiguateTypes.Invalid_choice (lazy (loc, - "The type of the term to be matched is not (co)inductive!")))) + "The type of the term to be matched is not (co)inductive: " + ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)))) in let _,leftsno,itl,_,indtyp_no = NCicEnvironment.get_checked_indtys indtype_ref in @@ -164,7 +185,7 @@ let interpretate_term List.nth itl indtyp_no with _ -> assert false in let rec count_prod t = - match NCicReduction.whd [] t with + match NCicReduction.whd ~subst:[] [] t with NCic.Prod (_, _, t) -> 1 + (count_prod t) | _ -> 0 in @@ -247,7 +268,7 @@ let interpretate_term | Some t -> aux ~localize loc context t in let cic_body = aux ~localize loc (cic_name :: context) body in - NCic.LetIn (cic_name, cic_def, cic_typ, cic_body) + NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false (* let context' = @@ -372,20 +393,27 @@ patterns not implemented *) in NCic.Meta (index, (0, NCic.Ctx cic_subst)) | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop - | CicNotationPt.Sort `Set -> assert false + | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type + [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) + | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type + [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) | CicNotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) - | _ -> assert false (* god bless Bologna *) + | CicNotationPt.Variable _ + | CicNotationPt.Magic _ + | CicNotationPt.Layout _ + | CicNotationPt.Literal _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) -> let res = aux_option ~localize loc context annotation (Some term) in - if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; + if localize then + NCicUntrusted.NCicHash.add localization_tbl res loc; res | Some (CicNotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) @@ -402,16 +430,12 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl ;; -let domain_of_term ~context = - Disambiguate.domain_of_ast_term ~context -;; - let disambiguate_term ~context ~metasenv ~subst ?goal ~mk_implicit ~description_of_alias ~mk_choice - ~aliases ~universe ~lookup_in_library + ~aliases ~universe ~coercion_db ~lookup_in_library (text,prefix_len,term) = - let localization_tbl = NCicUntrusted.NCicHash.create 503 in + let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let hint = match goal with None -> (fun _ y -> y),(fun x -> x) @@ -434,11 +458,50 @@ let disambiguate_term ~context ~metasenv ~subst ?goal ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:domain_of_term + ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl ~hint ~subst + ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term) + ~mk_localization_tbl ~hint ~subst in List.map (function (a,b,c,d,_) -> a,b,c,d) res, b ;; +let _ = +let mk_type n = + if n = 0 then + [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")] +in +let mk_cprop n = + if n = 0 then + [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")] + else + [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")] +in + NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1); + NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1); + NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1); + NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1); + NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0); + NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0); + + NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2); + NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2); + NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2); + NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2); + NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1); + NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1); + + NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3); + NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3); + NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3); + NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3); + NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2); + NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2); + + NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3); + NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); + +;; +