Big commit and major code clean-up:

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 76642ee3d51e553309d67b6294e4a475761b4613..42069ff5cb92ef6d6c7266d15c0725acc737937c 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -964,7 +964,91 @@ let type_of_aux' metasenv context term ugraph =
     type_of_aux' metasenv context term ugraph
   with 
     CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+
+(*CSC: this is a very very rough approximation; to be finished *)
+let are_all_occurrences_positive uri =
+ let rec aux =
+  (*CSC: here we should do a whd; but can we do that? *)
+  function
+     Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
+   | Cic.MutInd (uri',_,_) when uri = uri' -> ()
+   | Cic.Prod (_,_,t) -> aux t
+   | _ -> raise (RefineFailure "not well formed constructor type")
+ in
+  aux
     
+let typecheck metasenv uri obj =
+ let ugraph = CicUniv.empty_ugraph in
+ match obj with
+    Cic.Constant (name,Some bo,ty,args,attrs) ->
+     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+     let bo' = CicMetaSubst.apply_subst subst bo' in
+     let ty' = CicMetaSubst.apply_subst subst ty' in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+      Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
+  | Cic.Constant (name,None,ty,args,attrs) ->
+     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+      Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+  | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
+     assert (metasenv' = metasenv);
+     (* Here we do not check the metasenv for correctness *)
+     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+     let bo' = CicMetaSubst.apply_subst subst bo' in
+     let ty' = CicMetaSubst.apply_subst subst ty' in
+     let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+      Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
+  | Cic.Variable _ -> assert false (* not implemented *)
+  | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
+     (*CSC: this code is greately simplified and many many checks are missing *)
+     (*CSC: e.g. the constructors are not required to build their own types,  *)
+     (*CSC: the arities are not required to have as type a sort, etc.         *)
+     let uri = match uri with Some uri -> uri | None -> assert false in
+     let typesno = List.length tys in
+     (* first phase: we fix only the types *)
+     let metasenv,ugraph,tys =
+      List.fold_right
+       (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+         let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+          metasenv,ugraph,(name,b,ty',cl)::res
+       ) tys (metasenv,ugraph,[]) in
+     let con_context =
+      List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
+     (* second phase: we fix only the constructors *)
+     let metasenv,ugraph,tys =
+      List.fold_right
+       (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+         let metasenv,ugraph,cl' =
+          List.fold_right
+           (fun (name,ty) (metasenv,ugraph,res) ->
+             let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+             let ty',_,metasenv,ugraph =
+              type_of_aux' metasenv con_context ty ugraph in
+             let undebrujin t =
+              snd
+               (List.fold_right
+                 (fun (name,_,_,_) (i,t) ->
+                   (* here the explicit_named_substituion is assumed to be *)
+                   (* of length 0 *)
+                   let t' = Cic.MutInd (uri,i,[])  in
+                   let t = CicSubstitution.subst t' t in
+                    i - 1,t
+                 ) tys (typesno - 1,t)) in
+             let ty' = undebrujin ty in
+              metasenv,ugraph,(name,ty')::res
+           ) cl (metasenv,ugraph,[])
+         in
+          metasenv,ugraph,(name,b,ty,cl')::res
+       ) tys (metasenv,ugraph,[]) in
+     (* third phase: we check the positivity condition *)
+     List.iter
+      (fun (_,_,_,cl) ->
+        List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
+      ) tys ;
+     Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
 
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =