X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=4e3f8cac3e265aa362253b2dd47e440bfa97705e;hb=fdab21f9db0c8536718001e38213c34595170182;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..4e3f8cac3 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
@@ -60,9 +69,9 @@ let find_in_context name context =
   in
   aux 1 context
 
-let interpretate_term 
-  ?(create_dummy_ids=false) ~mk_choice ~context ~env ~uri ~is_path ast 
-  ~localization_tbl
+let interpretate_term_and_interpretate_term_option 
+  ?(create_dummy_ids=false) 
+    ~obj_context ~mk_choice ~env ~uri ~is_path ~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,104 +268,8 @@ 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)
-    | CicNotationPt.LetRec (_kind, _defs, _body) ->
-       assert false (*
-        let context' =
-          List.fold_left
-            (fun acc (_, (name, _), _, _) ->
-              cic_name_of_name name :: acc)
-            context defs
-        in
-        let cic_body =
-         let unlocalized_body = aux ~localize:false loc context' body in
-         match unlocalized_body with
-            NCic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
-          | NCic.Appl (NCic.Rel n::l) when n <= List.length defs ->
-             (try
-               let l' =
-                List.map
-                 (function t ->
-                   let t',subst,metasenv =
-                    CicMetaSubst.delift_rels [] [] (List.length defs) t
-                   in
-                    assert (subst=[]);
-                    assert (metasenv=[]);
-                    t') l
-               in
-                (* We can avoid the LetIn. But maybe we need to recompute l'
-                   so that it is localized *)
-                if localize then
-                 match body with
-                    CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
-                     (* since we avoid the letin, the context has no
-                      * recfuns in it *)
-                     let l' = List.map (aux ~localize loc context) l in
-                      `AvoidLetIn (n,l')
-                  | _ -> assert false
-                else
-                 `AvoidLetIn (n,l')
-              with
-               CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
-                if localize then
-                 `AddLetIn (aux ~localize loc context' body)
-                else
-                 `AddLetIn unlocalized_body)
-          | _ ->
-             if localize then
-              `AddLetIn (aux ~localize loc context' body)
-             else
-              `AddLetIn unlocalized_body
-        in
-        let inductiveFuns =
-          List.map
-            (fun (params, (name, typ), body, decr_idx) ->
-              let add_binders kind t =
-               List.fold_right
-                (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
-              in
-              let cic_body =
-               aux ~localize loc context' (add_binders `Lambda body) in
-              let cic_type =
-               aux_option ~localize loc context (Some `Type)
-                (HExtlib.map_option (add_binders `Pi) typ) in
-              let name =
-                match cic_name_of_name name with
-                | NCic.Anonymous ->
-                    CicNotationPt.fail loc
-                      "Recursive functions cannot be anonymous"
-                | NCic.Name name -> name
-              in
-              (name, decr_idx, cic_type, cic_body))
-            defs
-        in
-        let fix_or_cofix n =
-         match kind with
-            `Inductive -> NCic.Fix (n,inductiveFuns)
-          | `CoInductive ->
-              let coinductiveFuns =
-                List.map
-                 (fun (name, _, typ, body) -> name, typ, body)
-                 inductiveFuns
-              in
-               NCic.CoFix (n,coinductiveFuns)
-        in
-         let counter = ref ~-1 in
-         let build_term _ (var,_,ty,_) t =
-          incr counter;
-          NCic.LetIn (NCic.Name var, fix_or_cofix !counter, ty, t)
-         in
-          (match cic_body with
-              `AvoidLetInNoAppl n ->
-                let n' = List.length inductiveFuns - n in
-                 fix_or_cofix n'
-            | `AvoidLetIn (n,l) ->
-                let n' = List.length inductiveFuns - n in
-                 NCic.Appl (fix_or_cofix n'::l)
-            | `AddLetIn cic_body ->         
-                List.fold_right (build_term inductiveFuns) inductiveFuns
-                 cic_body)
-*)
+        NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
+    | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false 
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
@@ -352,7 +277,9 @@ let interpretate_term
        (try
          NCic.Rel (find_in_context name context)
        with Not_found -> 
-         Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
+         try NCic.Const (List.assoc name obj_context)
+         with Not_found ->
+           Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
     | CicNotationPt.Uri (name, subst) ->
        assert (subst = None);
        (try
@@ -372,46 +299,226 @@ 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)
     | Some CicNotationPt.Implicit -> NCic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
-   aux ~localize:true HExtlib.dummy_floc context ast
+   (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
+   (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
+;;
 
 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
-     ~localization_tbl
+     ~obj_context ~localization_tbl ~mk_choice
+=
+  let context = List.map fst context in
+  fst 
+    (interpretate_term_and_interpretate_term_option 
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+    ~context ast
+;;
+
+let interpretate_term_option 
+  ?(create_dummy_ids=false) ~context ~env ~uri ~is_path 
+  ~localization_tbl ~mk_choice ~obj_context
 =
   let context = List.map fst context in
-  interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
-~localization_tbl
+  snd 
+    (interpretate_term_and_interpretate_term_option 
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path ~localization_tbl)
+    ~context 
 ;;
 
-let domain_of_term ~context = 
-  Disambiguate.domain_of_ast_term ~context
-;; 
+let new_flavour_of_flavour = function 
+  | `Definition -> `Definition
+  | `MutualDefinition -> `Definition 
+  | `Fact -> `Fact
+  | `Lemma -> `Lemma
+  | `Remark -> `Corollary
+  | `Theorem -> `Theorem
+  | `Variant -> `Corollary 
+  | `Axiom -> `Fact
+;;
+
+(*
+let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+     ~localization_tbl
+=
+ assert (context = []);
+ assert (is_path = false);
+ let interpretate_term ?(obj_context=[]) =
+  interpretate_term ~mk_choice ~localization_tbl ~obj_context in
+ let interpretate_term_option ?(obj_context=[]) =
+   interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
+ match obj with
+ | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+     let attrs = `Provided, new_flavour_of_flavour flavour in
+     let ty' = interpretate_term [] env None false ty in
+     let height = (* XXX calculate *) 0 in
+     uri, height, [], [], 
+     (match bo,flavour with
+        None,`Axiom ->
+         NCic.Constant (name,None,ty',attrs)
+      | Some bo,`Axiom -> assert false
+      | None,_ ->
+         NCic.Constant (name,NCic.Implicit None,ty',attrs)
+      | Some bo,_ ->
+         match bo with
+         | CicNotationPt.LetRec (kind, defs, _) ->
+             let inductive = kind = `Inductive in
+             let obj_context =
+               List.split 
+                 (List.fold_left
+                   (fun (i,acc) (_,(name,_),_,k) -> 
+                    ((name, NReference.reference_of_spec uri 
+                       (if inductive then NReference.Fix (i,k,0)
+                        else NReference.CoFix i)) :: acc)
+                   (0,[]) defs))
+             in
+             let inductiveFuns =
+               List.map
+                 (fun (params, (name, typ), body, decr_idx) ->
+                   let add_binders kind t =
+                    List.fold_right
+                     (fun var t -> 
+                        CicNotationPt.Binder (kind, var, t)) params t
+                   in
+                   let cic_body =
+                     interpretate_term ~context ~env ~uri:None ~is_path:false
+                       (add_binders `Lambda body) 
+                   in
+                   let cic_type =
+                     interpretate_term_option ~context ~env ~uri:None
+                       ~is_path:false `Type
+                       (HExtlib.map_option (add_binders `Pi) typ)
+                   in
+                   (name, decr_idx, cic_type, cic_body))
+                 defs
+             in
+             NCic.Fixpoint (inductive,inductiveFuns,attrs)
+         | bo -> 
+             let bo = 
+               interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo
+             in
+             NCic.Constant (name,Some bo,ty',attrs))
+  | _ -> assert false
+(*
+  | CicNotationPt.Inductive (params,tyl) ->
+     let uri = match uri with Some uri -> uri | None -> assert false in
+     let context,params =
+      let context,res =
+       List.fold_left
+        (fun (context,res) (name,t) ->
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
+        ) ([],[]) params
+      in
+       context,List.rev res in
+     let add_params =
+      List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
+     let obj_context =
+      snd (
+       List.fold_left
+        (*here the explicit_named_substituion is assumed to be of length 0 *)
+        (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
+        (0,[]) tyl) in
+     let tyl =
+      List.map
+       (fun (name,b,ty,cl) ->
+         let ty' = add_params (interpretate_term context env None false ty) in
+         let cl' =
+          List.map
+           (fun (name,ty) ->
+             let ty' =
+              add_params
+               (interpretate_term ~obj_context ~context ~env ~uri:None
+                 ~is_path:false ty)
+             in
+              name,ty'
+           ) cl
+         in
+          name,b,ty',cl'
+       ) tyl
+     in
+      Cic.InductiveDefinition (tyl,[],List.length params,[])
+  | CicNotationPt.Record (params,name,ty,fields) ->
+     let uri = match uri with Some uri -> uri | None -> assert false in
+     let context,params =
+      let context,res =
+       List.fold_left
+        (fun (context,res) (name,t) ->
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
+        ) ([],[]) params
+      in
+       context,List.rev res in
+     let add_params =
+      List.fold_right
+       (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
+     let ty' = add_params (interpretate_term context env None false ty) in
+     let fields' =
+      snd (
+       List.fold_left
+        (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
+     let concl =
+      (*here the explicit_named_substituion is assumed to be of length 0 *)
+      let mutind = Cic.MutInd (uri,0,[]) in
+      if params = [] then mutind
+      else
+       Cic.Appl
+        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
+     let con =
+      List.fold_left
+       (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
+       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,z) -> x,y,z) fields in
+      Cic.InductiveDefinition
+       (tyl,[],List.length params,[`Class (`Record field_names)])
+*)
+;;
+*)
 
 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 +541,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
-     ~interpretate_thing:(interpretate_term ~mk_choice (?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 ~obj_context:[] ~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);
+
+         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);
+
+;;
+