X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=9e9130857145c2bb84d74eb718c33625f78d0e3b;hb=6110532ca4a8e80f0e867500fcae92bf2f44b899;hp=8dd4bc634a60f74b85b24ae50fcbb6d2d711a45e;hpb=aa941d8c9c451264a721364db1e412b877d4a08f;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 8dd4bc634..9e9130857 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,17 +27,25 @@ 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 + ~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 @@ -61,20 +69,25 @@ let find_in_context name context = aux 1 context let interpretate_term - ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl + ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast + ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); let rec aux ~localize loc context = function + t -> + let res = + match t with | 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 - Disambiguate.resolve env (Symbol (symb, i)) ~args:cic_args () + Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) | CicNotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> @@ -86,8 +99,8 @@ let interpretate_term | `Pi | `Forall -> NCic.Prod (cic_name, cic_type, cic_body) | `Exists -> - Disambiguate.resolve env (Symbol ("exists", 0)) - ~args:[ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ] ()) + Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0)) + (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context `Term outtype in @@ -125,15 +138,17 @@ let interpretate_term let indtype_ref = match indty_ident with | Some (indty_ident, _) -> - (match Disambiguate.resolve env (Id indty_ident) () with - | NCic.Const r -> r + (match Disambiguate.resolve ~env ~mk_choice + (Id indty_ident) (`Args []) with + | 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 @@ -144,15 +159,26 @@ let interpretate_term "because it is an inductive type without constructors "^ "or because all patterns use wildcards"))) in - (match Disambiguate.resolve env (Id (fst_constructor branches)) () with - | NCic.Const r -> r +(* + 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 (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 @@ -161,7 +187,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 @@ -244,7 +270,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' = @@ -348,7 +374,8 @@ let interpretate_term assert (subst = None); (try NCic.Rel (find_in_context name context) - with Not_found -> Disambiguate.resolve env (Id name) ()) + with Not_found -> + Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) | CicNotationPt.Uri (name, subst) -> assert (subst = None); (try @@ -358,7 +385,8 @@ let interpretate_term | CicNotationPt.Implicit -> NCic.Implicit `Term | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole) patterns not implemented *) - | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (Num i) ~num () + | CicNotationPt.Num (num, i) -> + Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map @@ -367,19 +395,26 @@ 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 (`CProp _u) -> NCic.Sort (NCic.Type [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"]) | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve env (Symbol (symbol, instance)) () + Disambiguate.resolve ~env ~mk_choice + (Symbol (symbol, instance)) (`Args []) | _ -> assert false (* god bless Bologna *) + + in +(* prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] res); *) + res 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) @@ -396,15 +431,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 - ~aliases ~universe ~lookup_in_library + ~mk_implicit ~description_of_alias ~mk_choice + ~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) @@ -423,15 +455,36 @@ let disambiguate_term ~context ~metasenv ~subst ?goal MultiPassDisambiguator.disambiguate_thing ~freshen_thing:CicNotationUtil.freshen_term ~context ~metasenv ~initial_ugraph:() ~aliases + ~mk_implicit ~description_of_alias ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~mk_implicit:(function false -> NCic.Implicit `Term - | true -> NCic.Implicit `Closed) ~passes:(MultiPassDisambiguator.passes ()) - ~lookup_in_library ~domain_of_thing:domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) - ~refine_thing:refine_term (text,prefix_len,term) - ~localization_tbl ~hint ~subst + ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term + ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None)) + ~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); +;; +