type typ =
Var of int
+ | Unit
| Top
| TConst of typformerreference
| Arrow of typ * typ
type term =
Rel of int
+ | UnitTerm
| Const of reference
| Lambda of string * (* typ **) term
| Appl of term list
| 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
assert false (* TODO *)
| NCic.Meta _ -> assert false (* TODO *)
| NCic.Appl (he::_) -> classify_not_term status no_dep_prods context he
- | NCic.Rel _ -> `KindOrType
+ | NCic.Rel n ->
+ let rec find_sort typ =
+ match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
+ NCic.Sort NCic.Prop -> `Proposition
+ | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
+ | NCic.Sort (NCic.Type [`Type,_]) ->
+ (*CSC: we could be more precise distinguishing the user provided
+ minimal elements of the hierarchies and classify these
+ as `Kind *)
+ `KindOrType
+ | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
+ | NCic.Prod (_,_,t) ->
+ (* we skipped arguments of applications, so here we need to skip
+ products *)
+ find_sort t
+ | _ -> assert false (* NOT A SORT *)
+ in
+ (match List.nth context (n-1) with
+ _,NCic.Decl typ -> find_sort typ
+ | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
| NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
(match classify_not_term status true [] ty with
| `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
let rec kind_of status ~metasenv context k =
match NCicReduction.whd status ~subst:[] context k with
- | NCic.Sort _ -> Type
+ | NCic.Sort NCic.Type _ -> Type
+ | NCic.Sort _ -> assert false (* NOT A KIND *)
| NCic.Prod (b,s,t) ->
(* CSC: non-invariant assumed here about "_" *)
(match classify status ~metasenv context s with
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
let rec glue_ctx_typ ctx typ =
match ctx with
| [] -> typ
- | Some (_,`OfType so)::ctx -> Arrow (so,glue_ctx_typ ctx typ)
- | Some (name,`OfKind so)::ctx -> Forall (name,so,glue_ctx_typ ctx typ)
- | None::ctx -> Skip (glue_ctx_typ ctx typ)
+ | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
+ | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
+ | None::ctx -> glue_ctx_typ ctx (Skip typ)
;;
let rec split_typ_lambdas status n ~metasenv context typ =
| 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 ???? *)
| 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 *)
| 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 _
| `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)
| `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) =
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)
- | `KindOrType -> assert false (* TODO ??? *)
| `PropKind
| `Proposition -> status, None
- | `Type ->
+ | `Type
+ | `KindOrType (*???*) ->
let ty = typ_of status ~metasenv [] ty in
status,
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 [](* BAD! *) 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 *************************)
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
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
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)
| TermDefinition ((ctx,ty),bo) ->
let name = name_of_uri `FunctionName uri in
let namectx = namectx_of_ctx ctx in
- name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
+ (*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 =
projects / helm.git / blobdiff