diff --git a/.#commit.sh b/.#commit.sh deleted file mode 120000 index c759dde..0000000 --- a/.#commit.sh +++ /dev/null @@ -1 +0,0 @@ -bob@bobmatoMacBook-Pro.local.17126 \ No newline at end of file diff --git a/_build/check_term.cmi b/_build/check_term.cmi deleted file mode 100644 index 1bc65ea..0000000 Binary files a/_build/check_term.cmi and /dev/null differ diff --git a/_build/check_term.cmo b/_build/check_term.cmo deleted file mode 100644 index a9cd2a7..0000000 Binary files a/_build/check_term.cmo and /dev/null differ diff --git a/_build/check_term.inferred.cmi b/_build/check_term.inferred.cmi deleted file mode 100644 index 1b1ceae..0000000 Binary files a/_build/check_term.inferred.cmi and /dev/null differ diff --git a/_build/check_term.inferred.mli b/_build/check_term.inferred.mli deleted file mode 100644 index 6eaccb1..0000000 --- a/_build/check_term.inferred.mli +++ /dev/null @@ -1,12 +0,0 @@ -val kind_check : - Syntax.context -> - Syntax.fc_type -> Syntax.role -> Syntax.kind_and_role option -val type_cxt_check : - Syntax.context -> - Syntax.fc_type list -> ('a * Syntax.kind_and_role) list -> bool -val proof_check : - Syntax.context -> - Syntax.co_proof -> - Syntax.role -> - (Syntax.fc_type * Syntax.fc_type * Syntax.kind_and_role) option -val type_check : Syntax.context -> Syntax.fc_term -> Syntax.fc_type option diff --git a/_build/check_term.inferred.mli.depends b/_build/check_term.inferred.mli.depends deleted file mode 100644 index 1f0b645..0000000 --- a/_build/check_term.inferred.mli.depends +++ /dev/null @@ -1 +0,0 @@ -check_term.inferred.mli: Syntax diff --git a/_build/check_term.ml b/_build/check_term.ml deleted file mode 100644 index 928517f..0000000 --- a/_build/check_term.ml +++ /dev/null @@ -1,250 +0,0 @@ -open Syntax -open Util - - - -let rec kind_check (cxt : context) (ty : fc_type) - (r : role ): kind_and_role option = match ty with - |TyVar x -> - (try - let (BTVar (KR (k,r1))) = List.assoc x cxt - in - if - check_cxt cxt && sub_role r1 r then Some (KR (k,r)) - else None - with - |_ -> None ) - |TyConst TArrow -> - Some (KR(arrow_kind,r)) - |TyConst (TEquality k)-> - Some (KR(eq_kind k,r)) - |TyConst h -> - let s = string_of_type_constant h in - (try - let BTConst k = List.assoc s cxt in - if check_cxt cxt then - Some (KR (k,r)) - else None - with |_ -> None - ) - |TyApp (a,b) -> - (try - let Some (KR ((KArrow (KR(k1,r2),k2)),r1)) - = kind_check cxt a r in - let Some (KR (k1',r1')) - = kind_check cxt b (role_min r1 r2) in - if r = r1 && - k1 = k1' then - Some (KR(k2,r)) - else None - with | _ -> None - ) - |TyForall (a,kr,ty) -> - (try - let Some (KR (Star,r1)) - = kind_check ((a,BTVar kr ):: cxt ) ty r in - if r = r1 then - Some (KR(Star,r)) - else None - with | _ -> None - ) - - -let rec type_cxt_check cxt = - List.for_all2 (fun ty (s, KR(k,r)) -> - match kind_check cxt ty r with - Some _ -> true - | _ -> false - ) - -let rec proof_check - (cxt :context) - (proof : co_proof) - (r : role ): - (fc_type * fc_type * kind_and_role) option = - match proof with - | CPAssump (c, types) -> ( - try - let BCoer (delta, TyEq (ty1, ty2), r1) - = List.assoc c cxt in - let Some (KR (k,_)) = kind_check cxt ty1 r1 in - if type_cxt_check cxt types delta - && sub_role r1 r - then - Some ((type_subst_cxt delta types ty1) , - (type_subst_cxt delta types ty2) , - (KR (k,r))) - else - None - with - |_ -> None - ) - | CPRefl ty -> ( - try - let Some kr = kind_check cxt ty r in - Some (ty,ty, kr) - with _ -> None - ) - |CPSym proof -> ( - try - let Some (ty1,ty2,kr)= proof_check cxt proof r in - Some (ty2,ty1,kr) - with _ -> None - ) - |CPTrans (a,b) -> ( - match proof_check cxt a r , proof_check cxt b r with - | Some (ty1,ty2,kr), Some (ty2',ty3,kr') when - ty2 = ty2' && kr = kr' -> - Some (ty1,ty3,kr) - | _ -> None - ) - |CPApp (pf,pa) -> ( - try - let Some (ty1,ty2, KR(KArrow (KR(k1',r2'),k2'),r')) - = proof_check cxt pf r in - let Some (ty1',ty2', KR(k1'', r'')) = - proof_check cxt pa (role_min r' r2') in - if k1' = k1'' - && r = r' (* verbose check *) - then - Some ((ty1 |$ ty1'), (ty2 |$ ty2'), KR(k2',r')) - else None - with _ -> None - ) - |CPNth (n,pf) -> ( - try - let Some (ty1,ty2,KR(k',r')) - = proof_check cxt pf r in - (match list_of_type ty1, list_of_type ty2 with - |(ht1,lst1), (ht2,lst2) -> - if ht1 = ht2 - then - (match ht1 with - (* injective in normal datatype *) - TyConst (Datatype s) -> - let BTConst k =List.assoc s cxt in - let (KR (k',r1)) = nth_kind_arg k n in - if sub_role r1 r - then - Some - (List.nth lst1 n, - List.nth lst2 n,KR(k',r)) - else None - |_ -> None - ) - else None ) - with _ -> None - ) - |CPForall (a, (KR(k',r') as kr) ,pf) -> ( - try - let Some (ty1,ty2, KR (Star,_))= proof_check ((a, BTVar kr) ::cxt) pf r in - Some (TyForall (a, kr,ty1), TyForall (a,kr,ty2), - kr) - with _ -> None - ) - |CPInst (pf,ty) -> ( - try - let Some (TyForall(a1,(KR (k'',r'') as k1'),ty1'), - TyForall(a2,k2',ty2'), - KR(Star,r')) = proof_check cxt pf r in - if k1'= k2' then - let Some kr1 = kind_check cxt ty r'' - in - if kr1 = k1' then - Some (type_subst a1 ty1' ty, - type_subst a2 ty2' ty, KR(Star,r)) - else None - else None - with _ -> None - ) - -let rec type_check (cxt : context) - (term : fc_term) : fc_type option = match term with - | FCVar v -> ( - try - let BTermVar ty'= List.assoc v cxt in - Some ty' - with - Not_found -> None - ) - | FCLam (v, ty, term') -> - (type_check ((v, BTermVar ty) :: cxt) term') - | FCApp (t1, t2) -> ( - try - let Some (TyApp ((TyApp ((TyConst TArrow), ty1)), ty2)) = type_check cxt t1 in - let Some ty3 = type_check cxt t2 in - if ty1 = ty3 then - Some ty2 - else None - with _ -> None - ) - | FCTLam (a, kr, term') -> - (try - let Some ty1 = - type_check ((a,BTVar kr)::cxt) term' - in Some (TyForall (a,kr,ty1)) - with _ ->None - ) - | FCTApp (term', ty) ->( - let Some (TyForall (a',KR(k',r'),ty')) = - type_check cxt term' in - let Some (KR (k'',r'')) = - kind_check cxt ty r' in - Some (type_subst a' ty' ty) - ) - | FCDatacon s -> - (try - let BDataCon (ty_cxt,ty) = - List.assoc s cxt in - Some (datacon_type ty_cxt ty) - with _ -> None - ) - |FCCase (ty,term',branches) -> - None - | FCPLam (s,(TyEq (ty1,ty2) as eq_ty),term') -> - (try - let Some ty' = - type_check - ((s, BCoer ([],eq_ty, Code))::cxt) - term' in - (** we use role Code - to do the kind check since it's - the most general role - *) - match kind_check cxt ty1 Code, - kind_check cxt ty2 Code with - |Some (KR (k1,_)), Some (KR (k2,_)) when k1 = k2 -> - Some ((eq_ty_of_kind k1) - |$ ty1 |$ ty2 |$ ty') - |_ -> None - with _ -> None - ) - | FCPApp (term', proof) -> ( - try - let - Some (TyApp - ((TyApp - ((TyApp - ((TyConst (TEquality k)),tya)),tyb)) - ,sigma)) - = type_check cxt term' in - let Some (ty1,ty2, _ )= proof_check cxt proof Code in - if ty1 = tya && - ty2 = tyb - then - Some (sigma) - else - None - with _ -> None - ) - | FCCoer (term',proof) -> ( - try - let Some sigma1 = type_check cxt term' in - let Some (sigma1', sigma2', KR(Star,Type))= proof_check cxt proof Type in - - if sigma1' = sigma1 then - Some sigma2' - else None - with _ -> None - ) - diff --git a/_build/check_term.ml.depends b/_build/check_term.ml.depends deleted file mode 100644 index 8197a37..0000000 --- a/_build/check_term.ml.depends +++ /dev/null @@ -1 +0,0 @@ -check_term.ml: List Syntax Util diff --git a/_build/syntax.cmi b/_build/syntax.cmi deleted file mode 100644 index 58d6fd8..0000000 Binary files a/_build/syntax.cmi and /dev/null differ diff --git a/_build/syntax.cmo b/_build/syntax.cmo deleted file mode 100644 index 1bc2b47..0000000 Binary files a/_build/syntax.cmo and /dev/null differ diff --git a/_build/syntax.ml b/_build/syntax.ml deleted file mode 100644 index aa70010..0000000 --- a/_build/syntax.ml +++ /dev/null @@ -1,60 +0,0 @@ -type kind = Star | KArrow of kind_and_role * kind - -and role = Code | Type - -and kind_and_role = KR of kind * role - -and type_constant = - Datatype of string - | TFunction of string - | TArrow - | TEquality of kind - -and fc_type = - TyVar of string - | TyConst of type_constant - | TyApp of fc_type * fc_type - | TyForall of string * kind_and_role * fc_type - -and co_proof = - CPAssump of string * fc_type list - | CPRefl of fc_type - | CPSym of co_proof - | CPTrans of co_proof * co_proof - | CPApp of co_proof * co_proof - | CPNth of int * co_proof - | CPForall of string * kind_and_role * co_proof - | CPInst of co_proof * fc_type - -and eq_type = - TyEq of fc_type * fc_type - -and fc_term = - FCVar of string - | FCLam of string * fc_type * fc_term - | FCApp of fc_term * fc_term - | FCTLam of string * kind_and_role * fc_term - | FCTApp of fc_term * fc_type - | FCDatacon of string - | FCCase of fc_type * fc_term * branch list - | FCPLam of string * eq_type * fc_term - | FCPApp of fc_term * co_proof - | FCCoer of fc_term * co_proof - -and branch = - (** string is the constructor *) - Branch of string * fc_term - -and binder = bind_key * bind_value -and bind_key = string -and bind_value = - | BTVar of kind_and_role - | BTConst of kind - | BCoer of type_context * eq_type * role - | BTermVar of fc_type - | BDataCon of type_context * fc_type - -and context = binder list - -and type_context = (string * kind_and_role) list - diff --git a/_build/syntax.ml.depends b/_build/syntax.ml.depends deleted file mode 100644 index 23302bf..0000000 --- a/_build/syntax.ml.depends +++ /dev/null @@ -1 +0,0 @@ -syntax.ml: diff --git a/commit.sh b/commit.sh index a87f054..d6be47a 100644 --- a/commit.sh +++ b/commit.sh @@ -8,4 +8,8 @@ git push origin master # git remote add arthuraa https://github.com/arthuraa/cis670-project.git # git pull arthuraa master -# git rm syntax.ml \ No newline at end of file +# git rm syntax.ml + +git add -u + +# It deletes all removed files and updates what was modified. Just doesn't add new files. It's better because if you have a file named "deleted.txt" it will also be removed. \ No newline at end of file