X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=0efb49bff54f039f92b3ff1bbef997fe9091777b;hb=75620ca64e3038fcbebb51559fdc31b2e8a00f93;hp=03579afabb4091e3b07ae0ab01834faee73bc14a;hpb=8e65e5eb59904848a24506ffe55323fdcc8bf975;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 03579afab..0efb49bff 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,7 +27,8 @@ 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))); @@ -39,7 +40,12 @@ let refine_term metasenv subst context uri ~use_coercions:_ term _ ~localization 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 @@ -70,13 +76,11 @@ let interpretate_term 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 @@ -180,7 +184,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 @@ -392,22 +396,23 @@ patterns not implemented *) [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 *) - - in - prerr_endline (NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] - res); - res + | 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) @@ -424,16 +429,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) @@ -456,10 +457,10 @@ 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 ;; @@ -483,5 +484,16 @@ in 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 false (mk_cprop 2) (mk_type 2); + NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2); + ;;