Ast.AttributedTerm (`IdRef id, t)
;;
+let level_of_uri u =
+ let name = NUri.name_of_uri u in
+ assert(String.length name > String.length "Type");
+ String.sub name 4 (String.length name - 4)
+;;
+
(* CODICE c&p da NCicPp *)
let nast_of_cic0 status
~(idref:
idref (Ast.Meta
(n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l))
| NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
- | NCic.Sort NCic.Type _ -> idref (Ast.Sort `Set)
- (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0"
- | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
- | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
- | C.Sort (C.Type l) ->
- F.fprintf f "Max(";
- aux ctx (C.Sort (C.Type [List.hd l]));
- List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x])))
- (List.tl l);
- F.fprintf f ")"*)
- (* CSC: qua siamo grezzi *)
+ | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set)
+ | NCic.Sort NCic.Type ((`Type,u)::_) ->
+ idref(Ast.Sort (`NType (level_of_uri u)))
+ | NCic.Sort NCic.Type ((`CProp,u)::_) ->
+ idref(Ast.Sort (`NCProp (level_of_uri u)))
+ | NCic.Sort NCic.Type ((`Succ,u)::_) ->
+ idref(Ast.Sort (`NType (level_of_uri u ^ "+1")))
| NCic.Implicit `Hole -> idref (Ast.UserInput)
| NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
| NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
K.inductive_type = ty;
K.inductive_constructors = build_constructors seed cl
}
+in
+let build_fixpoint b seed =
+ fun (_,n,_,ty,t) ->
+ let t = nast_of_cic ~context:[] t in
+ let ty = nast_of_cic ~context:[] ty in
+ `Definition
+ { K.def_id = gen_id inductive_prefix seed;
+ K.def_name = Some n;
+ K.def_aref = "";
+ K.def_type = ty;
+ K.def_term = t;
+ }
in
let res =
match kind with
- | NCic.Fixpoint (is_rec, ifl, _) -> assert false
+ | NCic.Fixpoint (is_rec, ifl, _) ->
+ (gen_id object_prefix seed, [], conjectures,
+ `Joint
+ { K.joint_id = gen_id joint_prefix seed;
+ K.joint_kind =
+ if is_rec then
+ `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
+ else `CoRecursive;
+ K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
+ })
| NCic.Inductive (is_ind, lno, itl, _) ->
(gen_id object_prefix seed, [], conjectures,
`Joint
{ K.joint_id = gen_id joint_prefix seed;
- K.joint_kind = `Inductive lno;
+ K.joint_kind =
+ if is_ind then `Inductive lno else `CoInductive lno;
K.joint_defs = List.map (build_inductive is_ind seed) itl
})
| NCic.Constant (_,_,Some bo,ty,_) ->