X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=8b8a7b216c74e360238b183789ed2acdb3319c6c;hb=0b2cf1b25d45ffb80b27416e057a58e3dc3f257d;hp=ec2d1c1c3ec271148a985c22adb5a1980779793f;hpb=de80dc03fc495c4dbdb54a970645dae34cbed1e7;p=helm.git

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index ec2d1c1c3..8b8a7b216 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -38,6 +38,7 @@ type kind =
 
 type typ =
    Var of int
+ | Unit
  | Top
  | TConst of typformerreference
  | Arrow of typ * typ
@@ -47,6 +48,7 @@ type typ =
 
 type term =
    Rel of int
+ | UnitTerm
  | Const of reference
  | Lambda of string * (* typ **) term
  | Appl of term list
@@ -73,8 +75,8 @@ type obj_kind =
  | TypeDefinition of typ_former_def
  | TermDeclaration of term_former_decl
  | TermDefinition of term_former_def
- | LetRec of (string * typ * term) list
- (* inductive and records missing *)
+ | LetRec of obj_kind list
+ | Algebraic of (string * typ_context * (string * typ list) list) list
 
 type obj = NUri.uri * obj_kind
 
@@ -132,7 +134,7 @@ let rec classify_not_term status no_dep_prods context t =
         | `Proposition
         | `Type -> assert false (* IMPOSSIBLE *)
         | `Kind
-        | `KindOrType -> `KindOrType
+        | `KindOrType -> `Type
         | `PropKind -> `Proposition)
   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
@@ -202,16 +204,17 @@ let rec skip_args status ~metasenv context =
      match classify status ~metasenv context arg with
       | `KindOrType
       | `Type
-      | `Term `TypeFormer -> arg::skip_args status ~metasenv context (tl1,tl2)
+      | `Term `TypeFormer ->
+         Some arg::skip_args status ~metasenv context (tl1,tl2)
       | `Kind
       | `Proposition
-      | `PropKind -> unitty::skip_args status ~metasenv context (tl1,tl2)
+      | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
       | `Term _ -> assert false (* IMPOSSIBLE *)
 ;;
 
 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 
-type db = typ_context ReferenceMap.t
+type db = (typ_context * typ option) ReferenceMap.t
 
 class type g_status =
  object
@@ -276,7 +279,7 @@ let context_of_typformer status ~metasenv context =
   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
-     (try ReferenceMap.find ref status#extraction_db
+     (try fst (ReferenceMap.find ref status#extraction_db)
       with
        Not_found -> assert false (* IMPOSSIBLE *))
   | NCic.Match _ -> assert false (* TODO ???? *)
@@ -320,7 +323,8 @@ let rec typ_of status ~metasenv context k =
   | NCic.Appl (he::args) ->
      let he_context = context_of_typformer status ~metasenv context he in
      TAppl (typ_of status ~metasenv context he ::
-      List.map (typ_of status ~metasenv context)
+      List.map
+       (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
        (skip_args status ~metasenv context (List.rev he_context,args)))
   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
                                    otherwise NOT A TYPE *)
@@ -328,6 +332,34 @@ let rec typ_of status ~metasenv context k =
   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 ;;
 
+let rec fomega_subst k t1 =
+ function
+  | Var n ->
+     if k=n then t1
+     else if n < k then Var n
+     else Var (n-1)
+  | Top -> Top
+  | TConst ref -> TConst ref
+  | Unit -> Unit
+  | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
+  | Skip t -> Skip (fomega_subst (k+1) t1 t)
+  | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
+  | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
+
+let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
+
+let rec fomega_whd status ty =
+ match ty with
+ | TConst r ->
+    (match fomega_lookup status r with
+        None -> ty
+      | Some ty -> fomega_whd status ty)
+ | TAppl (TConst r::args) ->
+    (match fomega_lookup status r with
+        None -> ty
+      | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
+ | _ -> ty
+
 let rec term_of status ~metasenv context =
  function
   | NCic.Implicit _
@@ -348,6 +380,7 @@ let rec term_of status ~metasenv context =
        | `Term _ -> assert false (* IMPOSSIBLE *))
   | NCic.LetIn (b,ty,t,bo) ->
      (match classify status ~metasenv context t with
+       | `Term `TypeFormerOrTerm (* ???? *)
        | `Term `Term ->
           LetIn (b,term_of status ~metasenv context t,
            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
@@ -358,22 +391,121 @@ let rec term_of status ~metasenv context =
        | `Proposition
        | `Term `PropFormer
        | `Term `TypeFormer
-       | `Term `TypeFormerOrTerm
-       | `Term `Proof -> assert false (* NOT IN PROGRAMMING LANGUAGES? EXPAND IT ??? *))
+       | `Term `Proof ->
+         (* not in programming languages, we expand it *)
+         term_of status ~metasenv context
+          (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
   | NCic.Rel n -> Rel n
   | NCic.Const ref -> Const ref
   | NCic.Appl (he::args) ->
-     assert false (* TODO
+     eat_args status metasenv
+      (term_of status ~metasenv context he) context
+      (typ_of status ~metasenv context
+        (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
+      args
+(*
      let he_context = context_of_typformer status ~metasenv context he in
-     TAppl (typ_of status ~metasenv context he ::
-      List.map (typ_of status ~metasenv context)
-       (skip_args status ~metasenv context (List.rev he_context,args)))*)
+     let process_args he =
+      function
+         `Empty -> he
+       | `Inst tl -> Inst (process_args he tl)
+       | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
+     in
+     Appl (typ_of status ~metasenv context he ::
+      process_args (typ_of status ~metasenv context he)
+       (skip_term_args status ~metasenv context (List.rev he_context,args))
+*)
   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
                                    otherwise NOT A TYPE *)
   | NCic.Meta _ -> assert false (* TODO *)
   | NCic.Match (ref,_,t,pl) ->
      Match (ref,term_of status ~metasenv context t,
       List.map (term_of status ~metasenv context) pl)
+and eat_args status metasenv acc context tyhe =
+ function
+    [] -> acc
+  | arg::tl ->
+     let mk_appl f x =
+      match f with
+         Appl args -> Appl (args@[x])
+       | _ -> Appl [f;x]
+     in
+     match fomega_whd status tyhe with
+        Arrow (s,t) ->
+         let arg =
+          match s with
+             Unit -> UnitTerm
+           | _ -> term_of status ~metasenv context arg in
+         eat_args status metasenv (mk_appl acc arg) context t tl
+      | Forall (_,_,t) ->
+         eat_args status metasenv (Inst acc)
+          context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
+      | Skip t ->
+         eat_args status metasenv acc context t tl
+      | Top -> assert false (*TODO: HOW??*)
+      | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
+;;
+
+let obj_of_constant status ~metasenv uri height bo ty =
+  match classify status ~metasenv [] ty with
+    | `Kind ->
+        let ty = kind_of status ~metasenv [] ty in
+        let ctx0,res = split_kind_prods [] ty in
+        let ctx,bo =
+         split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
+        (match classify status ~metasenv ctx bo with
+          | `Type
+          | `KindOrType -> (* ?? no kind formers in System F_omega *)
+              let nicectx =
+               List.map2
+                (fun p1 n ->
+                  HExtlib.map_option (fun (_,k) ->
+                   (*CSC: BUG here, clashes*)
+                   String.uncapitalize (fst n),k) p1)
+                ctx0 ctx
+              in
+              (* BUG here: for mutual type definitions the spec is not good *)
+              let ref =
+               NReference.reference_of_spec uri (NReference.Def height) in
+              let bo = typ_of status ~metasenv ctx bo in
+               status#set_extraction_db
+                (ReferenceMap.add ref (nicectx,Some bo)
+                  status#extraction_db),
+               Some (uri,TypeDefinition((nicectx,res),bo))
+          | `Kind -> status, None
+          | `PropKind
+          | `Proposition -> status, None
+          | `Term _ -> assert false (* IMPOSSIBLE *))
+    | `PropKind
+    | `Proposition -> status, None
+    | `KindOrType (* ??? *)
+    | `Type ->
+       (* CSC: TO BE FINISHED, REF NON REGISTERED *)
+       let ty = typ_of status ~metasenv [] ty in
+        status,
+        Some (uri, TermDefinition (split_typ_prods [] ty,
+         term_of status ~metasenv [] bo))
+    | `Term _ -> assert false (* IMPOSSIBLE *)
+;;
+
+let obj_of_inductive status ~metasenv uri ind leftno il =
+ let tyl =
+  HExtlib.filter_map
+   (fun _,name,arity,cl ->
+     match classify_not_term status true [] arity with
+      | `Proposition
+      | `KindOrType
+      | `Type -> assert false (* IMPOSSIBLE *)
+      | `PropKind -> None
+      | `Kind ->
+          let arity = kind_of status ~metasenv [] arity in
+          let ctx,_ as res = split_kind_prods [] arity in
+           Some (name,ctx,[])
+   ) il
+ in
+  match tyl with
+     [] -> status,None
+   | _ -> status, Some (uri, Algebraic tyl)
 ;;
 
 let obj_of status (uri,height,metasenv,subst,obj_kind) =
@@ -387,7 +519,7 @@ let obj_of status (uri,height,metasenv,subst,obj_kind) =
             let ctx,_ as res = split_kind_prods [] ty in
             let ref = NReference.reference_of_spec uri NReference.Decl in
              status#set_extraction_db
-              (ReferenceMap.add ref ctx status#extraction_db),
+              (ReferenceMap.add ref (ctx,None) status#extraction_db),
              Some (uri, TypeDeclaration res)
         | `PropKind
         | `Proposition -> status, None
@@ -398,45 +530,23 @@ let obj_of status (uri,height,metasenv,subst,obj_kind) =
              Some (uri, TermDeclaration (split_typ_prods [] ty))
         | `Term _ -> assert false (* IMPOSSIBLE *))
    | NCic.Constant (_,_,Some bo,ty,_) ->
-      (match classify status ~metasenv [] ty with
-        | `Kind ->
-            let ty = kind_of status ~metasenv [] ty in
-            let ctx0,res = split_kind_prods [] ty in
-            let ctx,bo =
-             split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
-            (match classify status ~metasenv ctx bo with
-              | `Type
-              | `KindOrType -> (* ?? no kind formers in System F_omega *)
-                  let nicectx =
-                   List.map2
-                    (fun p1 n ->
-                      HExtlib.map_option (fun (_,k) ->
-                       (*CSC: BUG here, clashes*)
-                       String.uncapitalize (fst n),k) p1)
-                    ctx0 ctx
-                  in
-                  let ref =
-                   NReference.reference_of_spec uri (NReference.Def height) in
-                   status#set_extraction_db
-                    (ReferenceMap.add ref ctx0 status#extraction_db),
-                   Some (uri,TypeDefinition((nicectx,res),typ_of status ~metasenv ctx bo))
-              | `Kind -> status, None
-              | `PropKind
-              | `Proposition -> status, None
-              | `Term _ -> assert false (* IMPOSSIBLE *))
-        | `PropKind
-        | `Proposition -> status, None
-        | `KindOrType (* ??? *)
-        | `Type ->
-           (* CSC: TO BE FINISHED, REF NON REGISTERED *)
-           let ty = typ_of status ~metasenv [] ty in
-            status,
-            Some (uri, TermDefinition (split_typ_prods [] ty,
-             term_of status ~metasenv [] bo))
-        | `Term _ -> assert false (* IMPOSSIBLE *))
+      obj_of_constant status ~metasenv uri height bo ty
+   | NCic.Fixpoint (_fix_or_cofix,fs,_) ->
+      let status,objs =
+        List.fold_right
+         (fun (_,_name,_,ty,bo) (status,res) ->
+           let status,obj = obj_of_constant ~metasenv status uri height bo ty in
+            match obj with
+               None -> status,res (*CSC: PRETTY PRINT SOMETHING ERASED*)
+             | Some (_uri,obj) -> status,obj::res)
+           fs (status,[])
+      in
+       status, Some (uri,LetRec objs)
+   | NCic.Inductive (ind,leftno,il,_) ->
+      obj_of_inductive status ~metasenv uri ind leftno il
  with
   NotInFOmega ->
-   prerr_endline "NOT IN F_omega";
+   prerr_endline "-- NOT IN F_omega";
    status, None
 
 (************************ HASKELL *************************)
@@ -481,6 +591,7 @@ let rec pp_kind =
 let rec pp_typ status ctx =
  function
    Var n -> List.nth ctx (n-1)
+ | Unit -> "()"
  | Top -> assert false (* ??? *)
  | TConst ref -> pp_ref status ref
  | Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2
@@ -494,13 +605,50 @@ let rec pp_typ status ctx =
 let rec pp_term status ctx =
  function
    Rel n -> List.nth ctx (n-1)
+ | UnitTerm -> "()"
  | Const ref -> pp_ref status ref
  | Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")"
  | Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")"
  | LetIn (name,s,t) ->
     "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
     ")"
- | Match _ -> assert false (* TODO of reference * term * term list *)
+ | Match (r,matched,pl) ->
+    let constructors, leftno =
+     let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
+     let _,_,_,cl  = List.nth tys n in
+      cl,leftno
+    in
+    let rec eat_branch n ty pat =
+      match (ty, pat) with
+      | NCic.Prod (_, _, t), _ when n > 0 ->
+         eat_branch (pred n) t pat 
+      | NCic.Prod (_, _, t), Lambda (name, t') ->
+          (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
+          let cv, rhs = eat_branch 0 t t' in
+          name :: cv, rhs
+      | _, _ -> [], pat
+    in
+    let j = ref 0 in
+    let patterns =
+      try
+        List.map2
+          (fun (_, name, ty) pat ->
+            incr j;
+            name, eat_branch leftno ty pat
+          ) constructors pl
+      with Invalid_argument _ -> assert false
+    in
+   "case " ^ pp_term status ctx matched ^ " of\n" ^
+   String.concat "\n"
+    (List.map
+      (fun (name,(bound_names,rhs)) ->
+        let pattern,body =
+         (*CSC: BUG avoid name clashes *)
+         String.concat " " (String.capitalize name::bound_names),
+         pp_term status ((List.rev bound_names)@ctx) rhs
+        in
+         "  " ^ pattern ^ " -> " ^ body
+     ) patterns)
  | TLambda t -> pp_term status ctx t
  | Inst t -> pp_term status ctx t
 
@@ -511,7 +659,7 @@ type term_former_def = term_context * term * typ
 type term_former_decl = term_context * typ
 *)
 
-let pp_obj status (uri,obj_kind) =
+let rec pp_obj status (uri,obj_kind) =
  let pp_ctx ctx =
   String.concat " " (List.rev
    (List.fold_right (fun (x,_) l -> x@::l)
@@ -536,14 +684,32 @@ let pp_obj status (uri,obj_kind) =
  | TermDefinition ((ctx,ty),bo) ->
     let name = name_of_uri `FunctionName uri in
     let namectx = namectx_of_ctx ctx in
+    (*CSC: BUG here *)
     name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^
     name ^ " = " ^ pp_term status namectx bo
- | LetRec _ -> assert false (* TODO 
- (* inductive and records missing *)*)
+ | LetRec l ->
+    (*CSC: BUG always uses the name of the URI *)
+    String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
+ | Algebraic il ->
+    String.concat "\n"
+     (List.map
+      (fun _name,ctx,cl ->
+        (*CSC: BUG always uses the name of the URI *)
+        "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
+        String.concat " | " (List.map
+         (fun name,tys ->
+          capitalize `Constructor name ^
+           String.concat " " (List.map (pp_typ status []) tys)
+         ) cl
+      )) il)
+ (* inductive and records missing *)
 
 let haskell_of_obj status obj =
  let status, obj = obj_of status obj in
-  status,HExtlib.map_option (pp_obj status) obj
+  status,
+   match obj with
+      None -> "-- ERASED\n"
+    | Some obj -> pp_obj status obj ^ "\n"
 
 (*
 let rec typ_of context =