X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=4e3f8cac3e265aa362253b2dd47e440bfa97705e;hb=46b91f34b693dabbd351ba813f5190051b09a117;hp=bfe12cee70bf5174000fd9cd44ed6a539a43d1bc;hpb=7aaaee610ab145cb419de016fb69c633fdaa6cb4;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index bfe12cee7..4e3f8cac3 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -69,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);
@@ -269,103 +269,7 @@ let interpretate_term
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         NCic.LetIn (cic_name, cic_typ, cic_def, 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)
-*)
+    | CicNotationPt.LetRec (_kind, _defs, _body) -> assert false 
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
@@ -373,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
@@ -420,16 +326,193 @@ patterns not implemented *)
     | 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 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 ~coercion_db ~lookup_in_library 
@@ -459,7 +542,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
-     ~interpretate_thing:(interpretate_term ~mk_choice (?create_dummy_ids:None))
+     ~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